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 String.Pos
UTF-8
offsets. For diagnostics, one-based Lean.Position
s are used internally.
character
is accepted liberally: actual character := min(line length, character)
Instances For
- uri : Lean.Lsp.DocumentUri
- range : Lean.Lsp.Range
A Location
is a DocumentUri
and a Range
.
Instances For
- originSelectionRange? : Option Lean.Lsp.Range
- targetUri : Lean.Lsp.DocumentUri
- targetRange : Lean.Lsp.Range
- targetSelectionRange : Lean.Lsp.Range
Instances For
- title : String
Title of the command, like
save
. - 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.
Instances For
- range : Lean.Lsp.Range
- newText : String
The string to be inserted. For delete operations use an empty string.
Identifier for annotated edit.
WorkspaceEdit
has achangeAnnotations
field 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.
A textual edit applicable to a text document.
Instances For
An array of TextEdit
s to be performed in sequence.
Instances For
- uri : Lean.Lsp.DocumentUri
Instances For
- textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
- edits : Lean.Lsp.TextEditBatch
A batch of TextEdit
s to perform on a versioned text document.
Instances For
- 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.
Instances For
Options for CreateFile
and RenameFile
.
Instances For
Options for DeleteFile
.
Instances For
- uri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.CreateFile.Options
Instances For
- oldUri : Lean.Lsp.DocumentUri
- newUri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.CreateFile.Options
Instances For
- uri : Lean.Lsp.DocumentUri
- options? : Option Lean.Lsp.DeleteFile.Options
Instances For
- 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.
Instances For
- changes : Lean.RBMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare
Changes to existing resources.
- documentChanges : Array Lean.Lsp.DocumentChange
Depending on the client capability
workspace.workspaceEdit.resourceOperations
document changes are either an array ofTextDocumentEdit
s 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 aboveTextDocumentEdit
s mixed with create, rename and delete file / folder operations.Whether a client supports versioned document edits is expressed via
workspace.workspaceEdit.documentChanges
client capability.If a client neither supports
documentChanges
norworkspace.workspaceEdit.resourceOperations
then only plainTextEdit
s using thechanges
property are supported. - changeAnnotations : Lean.RBMap String Lean.Lsp.ChangeAnnotation compare
A map of change annotations that can be referenced in
AnnotatedTextEdit
s or create, rename and delete file / folder operations.Whether clients honor this property depends on the client capability
workspace.changeAnnotationSupport
.
A workspace edit represents changes to many resources managed in the workspace.
Instances For
Instances For
Instances For
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.
The workspace/applyEdit
request is sent from the server to the client to modify resource on the client side.
Instances For
- 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.
An item to transfer a text document from the client to the server.
Instances For
- textDocument : Lean.Lsp.TextDocumentIdentifier
- position : Lean.Lsp.Position
Instances For
- documentSelector? : Option Lean.Lsp.DocumentSelector
Instances For
- plaintext: Lean.Lsp.MarkupKind
- markdown: Lean.Lsp.MarkupKind
Instances For
Reference to the progress of some in-flight piece of work.
Instances For
- workDoneToken? : Option Lean.Lsp.ProgressToken
Instances For
- partialResultToken? : Option Lean.Lsp.ProgressToken