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.
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
offsets. For diagnostics, one-based
Lean.Positions are used internally.
character is accepted liberally: actual character := min(line length, character)
- title : String
Title of the command, like
- command : String
The identifier of the actual command handler.
Arguments that the command handler should be invoked with.
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.
- range : Lean.Lsp.Range
- newText : String
The string to be inserted. For delete operations use an empty string.
A textual edit applicable to a text document.
- 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.
Additional information that describes document changes.
- 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
A change to a file resource.
Changes to existing resources.
Depending on the client capability
workspace.workspaceEdit.resourceOperationsdocument changes are either an array of
TextDocumentEdits 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 above
TextDocumentEdits mixed with create, rename and delete file / folder operations.
Whether a client supports versioned document edits is expressed via
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
A workspace edit represents changes to many resources managed in the workspace.
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.
workspace/applyEdit request is sent from the server to the client to modify resource on the client side.
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.
An item to transfer a text document from the client to the server.
More detailed associated progress message.
- cancellable : Bool
Controls if a cancel button should show to allow the user to cancel the operation.
Optional progress percentage to display (value 100 is considered 100%). If not provided infinite progress is assumed.