Defines most of the 'Basic Structures' in the LSP specification (https://microsoft.github.io/language-server-protocol/specifications/specification-current/), as well as some utilities.
Since LSP is Json-based, Ints/Nats are represented by Floats on the wire.
Equations
- Lean.Lsp.instInhabitedCancelParams = { default := { id := default } }
Equations
Equations
- Lean.Lsp.instToJsonCancelParams = { toJson := Lean.Lsp.toJsonCancelParams✝ }
Equations
- Lean.Lsp.instFromJsonCancelParams = { fromJson? := Lean.Lsp.fromJsonCancelParams✝ }
We adopt the convention that zero-based UTF-16 positions as sent by LSP clients
are represented by Lsp.Position while internally we mostly use String.Pos UTF-8
offsets. For diagnostics, one-based Lean.Positions are used internally.
character is accepted liberally: actual character := min(line length, character)
Equations
- Lean.Lsp.instInhabitedPosition = { default := { line := default, character := default } }
Equations
- Lean.Lsp.instBEqPosition = { beq := Lean.Lsp.beqPosition✝ }
Equations
- Lean.Lsp.instOrdPosition = { compare := Lean.Lsp.ordPosition✝ }
Equations
- Lean.Lsp.instHashablePosition = { hash := Lean.Lsp.hashPosition✝ }
Equations
- Lean.Lsp.instToJsonPosition = { toJson := Lean.Lsp.toJsonPosition✝ }
Equations
- Lean.Lsp.instFromJsonPosition = { fromJson? := Lean.Lsp.fromJsonPosition✝ }
Equations
- Lean.Lsp.instToStringPosition = { toString := fun (p : Lean.Lsp.Position) => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")" }
Equations
- Lean.Lsp.instLTPosition = ltOfOrd
Equations
- Lean.Lsp.instLEPosition = leOfOrd
Equations
- Lean.Lsp.instInhabitedRange = { default := { start := default, «end» := default } }
Equations
- Lean.Lsp.instBEqRange = { beq := Lean.Lsp.beqRange✝ }
Equations
- Lean.Lsp.instHashableRange = { hash := Lean.Lsp.hashRange✝ }
Equations
- Lean.Lsp.instToJsonRange = { toJson := Lean.Lsp.toJsonRange✝ }
Equations
- Lean.Lsp.instFromJsonRange = { fromJson? := Lean.Lsp.fromJsonRange✝ }
Equations
- Lean.Lsp.instOrdRange = { compare := Lean.Lsp.ordRange✝ }
A Location is a DocumentUri and a Range.
- uri : Lean.Lsp.DocumentUri
- range : Lean.Lsp.Range
Equations
- Lean.Lsp.instInhabitedLocation = { default := { uri := default, range := default } }
Equations
- Lean.Lsp.instBEqLocation = { beq := Lean.Lsp.beqLocation✝ }
Equations
- Lean.Lsp.instToJsonLocation = { toJson := Lean.Lsp.toJsonLocation✝ }
Equations
- Lean.Lsp.instFromJsonLocation = { fromJson? := Lean.Lsp.fromJsonLocation✝ }
Equations
- Lean.Lsp.instOrdLocation = { compare := Lean.Lsp.ordLocation✝ }
- originSelectionRange? : Option Lean.Lsp.Range
- targetUri : Lean.Lsp.DocumentUri
- targetRange : Lean.Lsp.Range
- targetSelectionRange : Lean.Lsp.Range
Equations
- Lean.Lsp.instToJsonLocationLink = { toJson := Lean.Lsp.toJsonLocationLink✝ }
Equations
- Lean.Lsp.instFromJsonLocationLink = { fromJson? := Lean.Lsp.fromJsonLocationLink✝ }
Represents a reference to a client editor command.
NOTE: No specific commands are specified by LSP, hence possible commands need to be announced as capabilities.
Equations
- Lean.Lsp.instToJsonCommand = { toJson := Lean.Lsp.toJsonCommand✝ }
Equations
- Lean.Lsp.instFromJsonCommand = { fromJson? := Lean.Lsp.fromJsonCommand✝ }
A snippet is a string that gets inserted into a document, and can afterwards be edited by the user in a structured way.
Snippets contain instructions that specify how this structured editing should proceed. They are expressed in a domain-specific language based on one from TextMate, including the following constructs:
- Designated positions for subsequent user input,
called "tab stops" after their most frequently-used keybinding.
They are denoted with
$1,$2, and so forth.$0denotes where the cursor should be positioned after all edits are completed, defaulting to the end of the string. Snippet tab stops are unrelated to tab stops used for indentation. - Tab stops with default values, called placeholders, written
${1:default}. The default may itself contain a tab stop or a further placeholder and multiple options to select from may be provided by surrounding them with|s and separating them with,, as in${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}. - One of a set of predefined variables that are replaced with their values.
This includes the current line number (
$TM_LINE_NUMBER) or the text that was selected when the snippet was invoked ($TM_SELECTED_TEXT). - Formatting instructions to modify variables using regular expressions or a set of predefined filters.
The full syntax and semantics of snippets, including the available variables and the rules for escaping control characters, are described in the LSP specification.
- value : String
Equations
- Lean.Lsp.instToJsonSnippetString = { toJson := Lean.Lsp.toJsonSnippetString✝ }
Equations
- Lean.Lsp.instFromJsonSnippetString = { fromJson? := Lean.Lsp.fromJsonSnippetString✝ }
A textual edit applicable to a text document.
- range : Lean.Lsp.Range
- newText : String
The string to be inserted. For delete operations use an empty string.
- leanExtSnippet? : Option Lean.Lsp.SnippetString
If this field is present and the editor supports it,
newTextis ignored and an interactive snippet edit is performed instead.The use of snippets in
TextEdits is a Lean-specific extension to the LSP standard, sonewTextshould still be set to a correct value as fallback in case the editor does not support this feature. Even editors that support snippets may not always use them; for instance, if the file is not already open, VS Code will perform a normal text edit in the background instead. Identifier for annotated edit.
WorkspaceEdithas achangeAnnotationsfield that maps these identifiers to aChangeAnnotation. By annotating an edit you can add a description of what the edit will do and also control whether the user is presented with a prompt before applying the edit. reference.
Equations
- Lean.Lsp.instToJsonTextEdit = { toJson := Lean.Lsp.toJsonTextEdit✝ }
Equations
- Lean.Lsp.instFromJsonTextEdit = { fromJson? := Lean.Lsp.fromJsonTextEdit✝ }
An array of TextEdits to be performed in sequence.
Equations
Equations
- Lean.Lsp.instFromJsonTextEditBatch = { fromJson? := Lean.fromJson? }
Equations
- Lean.Lsp.instToJsonTextEditBatch = { toJson := Lean.toJson }
Equations
- Lean.Lsp.instEmptyCollectionTextEditBatch = { emptyCollection := #[] }
Equations
- Lean.Lsp.instCoeTextEditTextEditBatch = { coe := fun (te : Lean.Lsp.TextEdit) => #[te] }
A batch of TextEdits to perform on a versioned text document.
- textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
- edits : Lean.Lsp.TextEditBatch
Equations
Equations
- Lean.Lsp.instFromJsonTextDocumentEdit = { fromJson? := Lean.Lsp.fromJsonTextDocumentEdit✝ }
Additional information that describes document changes.
- label : String
A human-readable string describing the actual change. The string is rendered prominent in the user interface.
- needsConfirmation : Bool
A flag which indicates that user confirmation is needed before applying the change.
A human-readable string which is rendered less prominent in the user interface.
Equations
Equations
- Lean.Lsp.instFromJsonChangeAnnotation = { fromJson? := Lean.Lsp.fromJsonChangeAnnotation✝ }
Options for CreateFile and RenameFile.
Options for DeleteFile.
- uri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.CreateFile.Options
Equations
- Lean.Lsp.instToJsonCreateFile = { toJson := Lean.Lsp.toJsonCreateFile✝ }
Equations
- Lean.Lsp.instFromJsonCreateFile = { fromJson? := Lean.Lsp.fromJsonCreateFile✝ }
- oldUri : Lean.Lsp.DocumentUri
- newUri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.CreateFile.Options
Equations
- Lean.Lsp.instToJsonRenameFile = { toJson := Lean.Lsp.toJsonRenameFile✝ }
Equations
- Lean.Lsp.instFromJsonRenameFile = { fromJson? := Lean.Lsp.fromJsonRenameFile✝ }
- uri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.DeleteFile.Options
Equations
- Lean.Lsp.instToJsonDeleteFile = { toJson := Lean.Lsp.toJsonDeleteFile✝ }
Equations
- Lean.Lsp.instFromJsonDeleteFile = { fromJson? := Lean.Lsp.fromJsonDeleteFile✝ }
A change to a file resource.
- create : Lean.Lsp.CreateFile → Lean.Lsp.DocumentChange
- rename : Lean.Lsp.RenameFile → Lean.Lsp.DocumentChange
- delete : Lean.Lsp.DeleteFile → Lean.Lsp.DocumentChange
- edit : Lean.Lsp.TextDocumentEdit → Lean.Lsp.DocumentChange
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A workspace edit represents changes to many resources managed in the workspace.
- changes? : Option (Lean.RBMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare)
Changes to existing resources.
- documentChanges? : Option (Array Lean.Lsp.DocumentChange)
Depending on the client capability
workspace.workspaceEdit.resourceOperationsdocument changes are either an array ofTextDocumentEdits to express changes to n different text documents where each text document edit addresses a specific version of a text document. Or it can contain aboveTextDocumentEdits mixed with create, rename and delete file / folder operations.Whether a client supports versioned document edits is expressed via
workspace.workspaceEdit.documentChangesclient capability.If a client neither supports
documentChangesnorworkspace.workspaceEdit.resourceOperationsthen only plainTextEdits using thechangesproperty are supported. - changeAnnotations? : Option (Lean.RBMap String Lean.Lsp.ChangeAnnotation compare)
A map of change annotations that can be referenced in
AnnotatedTextEdits or create, rename and delete file / folder operations.Whether clients honor this property depends on the client capability
workspace.changeAnnotationSupport.
Equations
- Lean.Lsp.instToJsonWorkspaceEdit = { toJson := Lean.Lsp.toJsonWorkspaceEdit✝ }
Equations
- Lean.Lsp.instFromJsonWorkspaceEdit = { fromJson? := Lean.Lsp.fromJsonWorkspaceEdit✝ }
Equations
- Lean.Lsp.WorkspaceEdit.instEmptyCollection = { emptyCollection := { changes? := none, documentChanges? := none, changeAnnotations? := none } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit e = { changes? := none, documentChanges? := some #[Lean.Lsp.DocumentChange.edit e], changeAnnotations? := none }
Equations
- Lean.Lsp.WorkspaceEdit.ofTextEdit doc te = Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit { textDocument := doc, edits := #[te] }
The workspace/applyEdit request is sent from the server to the client to modify resource on the client side.
An optional label of the workspace edit. This label is presented in the user interface for example on an undo stack to undo the workspace edit.
- edit : Lean.Lsp.WorkspaceEdit
The edits to apply.
An item to transfer a text document from the client to the server.
- uri : Lean.Lsp.DocumentUri
The text document's URI.
- languageId : String
The text document's language identifier.
- version : Nat
The version number of this document (it will increase after each change, including undo/redo).
- text : String
The content of the opened text document.
Equations
Equations
- Lean.Lsp.instFromJsonTextDocumentItem = { fromJson? := Lean.Lsp.fromJsonTextDocumentItem✝ }
- textDocument : Lean.Lsp.TextDocumentIdentifier
- position : Lean.Lsp.Position
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Lsp.instToJsonDocumentFilter = { toJson := Lean.Lsp.toJsonDocumentFilter✝ }
Equations
- Lean.Lsp.instFromJsonDocumentFilter = { fromJson? := Lean.Lsp.fromJsonDocumentFilter✝ }
Equations
- Lean.Lsp.instFromJsonDocumentSelector = { fromJson? := Lean.fromJson? }
Equations
- Lean.Lsp.instToJsonDocumentSelector = { toJson := Lean.toJson }
- documentSelector? : Option Lean.Lsp.DocumentSelector
- plaintext : Lean.Lsp.MarkupKind
- markdown : Lean.Lsp.MarkupKind
Equations
- Lean.Lsp.instDecidableEqMarkupKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Lean.Lsp.instHashableMarkupKind = { hash := Lean.Lsp.hashMarkupKind✝ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- kind : Lean.Lsp.MarkupKind
- value : String
Equations
- Lean.Lsp.instToJsonMarkupContent = { toJson := Lean.Lsp.toJsonMarkupContent✝ }
Equations
- Lean.Lsp.instFromJsonMarkupContent = { fromJson? := Lean.Lsp.fromJsonMarkupContent✝ }
Equations
Reference to the progress of some in-flight piece of work.
Equations
Equations
- Lean.Lsp.instToJsonProgressParams = { toJson := Lean.Lsp.toJsonProgressParams✝ }
- workDoneToken? : Option Lean.Lsp.ProgressToken
- partialResultToken? : Option Lean.Lsp.ProgressToken
- workDoneProgress : Bool