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.

@[reducible, inline]

abbrev Lean.Lsp.DocumentUri : Type

structure Lean.Lsp.Position : Type

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)

• line : Nat
• character : Nat

instance Lean.Lsp.instInhabitedPosition : Inhabited Position

instance Lean.Lsp.instBEqPosition : BEq Position

instance Lean.Lsp.instOrdPosition : Ord Position

instance Lean.Lsp.instHashablePosition : Hashable Position

instance Lean.Lsp.instToJsonPosition : ToJson Position

instance Lean.Lsp.instFromJsonPosition : FromJson Position

instance Lean.Lsp.instReprPosition : Repr Position

instance Lean.Lsp.instToStringPosition : ToString Position

instance Lean.Lsp.instLTPosition : LT Position

instance Lean.Lsp.instLEPosition : LE Position

structure Lean.Lsp.Range : Type

• start : Position
• end : Position

instance Lean.Lsp.instInhabitedRange : Inhabited Range

instance Lean.Lsp.instBEqRange : BEq Range

instance Lean.Lsp.instHashableRange : Hashable Range

instance Lean.Lsp.instToJsonRange : ToJson Range

instance Lean.Lsp.instFromJsonRange : FromJson Range

instance Lean.Lsp.instOrdRange : Ord Range

instance Lean.Lsp.instReprRange : Repr Range

instance Lean.Lsp.instLTRange : LT Range

instance Lean.Lsp.instLERange : LE Range

structure Lean.Lsp.Location : Type

A Location is a DocumentUri and a Range.

• uri : DocumentUri
• range : Range

instance Lean.Lsp.instInhabitedLocation : Inhabited Location

instance Lean.Lsp.instBEqLocation : BEq Location

instance Lean.Lsp.instToJsonLocation : ToJson Location

instance Lean.Lsp.instFromJsonLocation : FromJson Location

instance Lean.Lsp.instOrdLocation : Ord Location

structure Lean.Lsp.LocationLink : Type

• originSelectionRange? : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range

instance Lean.Lsp.instToJsonLocationLink : ToJson LocationLink

instance Lean.Lsp.instFromJsonLocationLink : FromJson LocationLink

structure Lean.Lsp.Command : Type

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.

reference

• title : String

  Title of the command, like save.

• command : String

  The identifier of the actual command handler.

• arguments? : Option (Array Json)

  Arguments that the command handler should be invoked with.

instance Lean.Lsp.instToJsonCommand : ToJson Command

instance Lean.Lsp.instFromJsonCommand : FromJson Command

structure Lean.Lsp.SnippetString : Type

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. $0 denotes 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

instance Lean.Lsp.instToJsonSnippetString : ToJson SnippetString

instance Lean.Lsp.instFromJsonSnippetString : FromJson SnippetString

structure Lean.Lsp.TextEdit : Type

A textual edit applicable to a text document.

reference

• range : Range

  The range of the text document to be manipulated. To insert text into a document create a range where start = end.

• newText : String

  The string to be inserted. For delete operations use an empty string.

• leanExtSnippet? : Option SnippetString

  If this field is present and the editor supports it, newText is ignored and an interactive snippet edit is performed instead.

  The use of snippets in TextEdits is a Lean-specific extension to the LSP standard, so newText should 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.

• annotationId? : Option String

  Identifier for annotated edit.

  WorkspaceEdit has a changeAnnotations field that maps these identifiers to a ChangeAnnotation. 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.

instance Lean.Lsp.instToJsonTextEdit : ToJson TextEdit

instance Lean.Lsp.instFromJsonTextEdit : FromJson TextEdit

def Lean.Lsp.TextEditBatch : Type

An array of TextEdits to be performed in sequence.

instance Lean.Lsp.instFromJsonTextEditBatch : FromJson TextEditBatch

instance Lean.Lsp.instToJsonTextEditBatch : ToJson TextEditBatch

instance Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection TextEditBatch

instance Lean.Lsp.instAppendTextEditBatch : Append TextEditBatch

instance Lean.Lsp.instCoeTextEditTextEditBatch : Coe TextEdit TextEditBatch

structure Lean.Lsp.TextDocumentIdentifier : Type

• uri : DocumentUri

instance Lean.Lsp.instToJsonTextDocumentIdentifier : ToJson TextDocumentIdentifier

instance Lean.Lsp.instFromJsonTextDocumentIdentifier : FromJson TextDocumentIdentifier

structure Lean.Lsp.VersionedTextDocumentIdentifier : Type

• uri : DocumentUri
• version? : Option Nat

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : ToJson VersionedTextDocumentIdentifier

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : FromJson VersionedTextDocumentIdentifier

structure Lean.Lsp.TextDocumentEdit : Type

A batch of TextEdits to perform on a versioned text document.

reference

• textDocument : VersionedTextDocumentIdentifier
• edits : TextEditBatch

instance Lean.Lsp.instToJsonTextDocumentEdit : ToJson TextDocumentEdit

instance Lean.Lsp.instFromJsonTextDocumentEdit : FromJson TextDocumentEdit

structure Lean.Lsp.ChangeAnnotation : Type

Additional information that describes document changes.

reference

• 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.

• description? : Option String

  A human-readable string which is rendered less prominent in the user interface.

instance Lean.Lsp.instToJsonChangeAnnotation : ToJson ChangeAnnotation

instance Lean.Lsp.instFromJsonChangeAnnotation : FromJson ChangeAnnotation

structure Lean.Lsp.CreateFile.Options : Type

Options for CreateFile and RenameFile.

• overwrite : Bool
• ignoreIfExists : Bool

instance Lean.Lsp.CreateFile.instToJsonOptions : ToJson Options

instance Lean.Lsp.CreateFile.instFromJsonOptions : FromJson Options

structure Lean.Lsp.DeleteFile.Options : Type

Options for DeleteFile.

• recursive : Bool
• ignoreIfNotExists : Bool

instance Lean.Lsp.DeleteFile.instToJsonOptions : ToJson Options

instance Lean.Lsp.DeleteFile.instFromJsonOptions : FromJson Options

structure Lean.Lsp.CreateFile : Type

• uri : DocumentUri
• options? : Option Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonCreateFile : ToJson CreateFile

instance Lean.Lsp.instFromJsonCreateFile : FromJson CreateFile

structure Lean.Lsp.RenameFile : Type

• oldUri : DocumentUri
• newUri : DocumentUri
• options? : Option CreateFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonRenameFile : ToJson RenameFile

instance Lean.Lsp.instFromJsonRenameFile : FromJson RenameFile

structure Lean.Lsp.DeleteFile : Type

• uri : DocumentUri
• options? : Option Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonDeleteFile : ToJson DeleteFile

instance Lean.Lsp.instFromJsonDeleteFile : FromJson DeleteFile

inductive Lean.Lsp.DocumentChange : Type

A change to a file resource.

reference

• create : CreateFile → DocumentChange
• rename : RenameFile → DocumentChange
• delete : DeleteFile → DocumentChange
• edit : TextDocumentEdit → DocumentChange

instance Lean.Lsp.instToJsonDocumentChange : ToJson DocumentChange

instance Lean.Lsp.instFromJsonDocumentChange : FromJson DocumentChange

structure Lean.Lsp.WorkspaceEdit : Type

A workspace edit represents changes to many resources managed in the workspace.

reference

• changes? : Option (RBMap DocumentUri TextEditBatch compare)

  Changes to existing resources.

• documentChanges? : Option (Array DocumentChange)

  Depending on the client capability workspace.workspaceEdit.resourceOperations document 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 workspace.workspaceEdit.documentChanges client capability.

  If a client neither supports documentChanges nor workspace.workspaceEdit.resourceOperations then only plain TextEdits using the changes property are supported.

• changeAnnotations? : Option (RBMap String 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.

instance Lean.Lsp.instToJsonWorkspaceEdit : ToJson WorkspaceEdit

instance Lean.Lsp.instFromJsonWorkspaceEdit : FromJson WorkspaceEdit

instance Lean.Lsp.WorkspaceEdit.instEmptyCollection : EmptyCollection WorkspaceEdit

instance Lean.Lsp.WorkspaceEdit.instAppend : Append WorkspaceEdit

def Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit (e : TextDocumentEdit) : WorkspaceEdit

def Lean.Lsp.WorkspaceEdit.ofTextEdit (doc : VersionedTextDocumentIdentifier) (te : TextEdit) : WorkspaceEdit

structure Lean.Lsp.ApplyWorkspaceEditParams : Type

The workspace/applyEdit request is sent from the server to the client to modify resource on the client side.

reference

• label? : Option String

  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 : WorkspaceEdit

  The edits to apply.

instance Lean.Lsp.instToJsonApplyWorkspaceEditParams : ToJson ApplyWorkspaceEditParams

instance Lean.Lsp.instFromJsonApplyWorkspaceEditParams : FromJson ApplyWorkspaceEditParams

structure Lean.Lsp.TextDocumentItem : Type

An item to transfer a text document from the client to the server.

reference

• uri : 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.

instance Lean.Lsp.instToJsonTextDocumentItem : ToJson TextDocumentItem

instance Lean.Lsp.instFromJsonTextDocumentItem : FromJson TextDocumentItem

structure Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instToJsonTextDocumentPositionParams : ToJson TextDocumentPositionParams

instance Lean.Lsp.instFromJsonTextDocumentPositionParams : FromJson TextDocumentPositionParams

instance Lean.Lsp.instToStringTextDocumentPositionParams : ToString TextDocumentPositionParams

structure Lean.Lsp.DocumentFilter : Type

• language? : Option String
• scheme? : Option String
• pattern? : Option String

instance Lean.Lsp.instToJsonDocumentFilter : ToJson DocumentFilter

instance Lean.Lsp.instFromJsonDocumentFilter : FromJson DocumentFilter

def Lean.Lsp.DocumentSelector : Type

instance Lean.Lsp.instFromJsonDocumentSelector : FromJson DocumentSelector

instance Lean.Lsp.instToJsonDocumentSelector : ToJson DocumentSelector

structure Lean.Lsp.StaticRegistrationOptions : Type

• id? : Option String

instance Lean.Lsp.instToJsonStaticRegistrationOptions : ToJson StaticRegistrationOptions

instance Lean.Lsp.instFromJsonStaticRegistrationOptions : FromJson StaticRegistrationOptions

structure Lean.Lsp.TextDocumentRegistrationOptions : Type

• documentSelector? : Option DocumentSelector

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions : ToJson TextDocumentRegistrationOptions

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : FromJson TextDocumentRegistrationOptions

inductive Lean.Lsp.MarkupKind : Type

• plaintext : MarkupKind
• markdown : MarkupKind

instance Lean.Lsp.instDecidableEqMarkupKind : DecidableEq MarkupKind

instance Lean.Lsp.instHashableMarkupKind : Hashable MarkupKind

instance Lean.Lsp.instFromJsonMarkupKind : FromJson MarkupKind

instance Lean.Lsp.instToJsonMarkupKind : ToJson MarkupKind

structure Lean.Lsp.MarkupContent : Type

• kind : MarkupKind
• value : String

instance Lean.Lsp.instToJsonMarkupContent : ToJson MarkupContent

instance Lean.Lsp.instFromJsonMarkupContent : FromJson MarkupContent

instance Lean.Lsp.instDecidableEqMarkupContent : DecidableEq MarkupContent

instance Lean.Lsp.instHashableMarkupContent : Hashable MarkupContent

@[reducible, inline]

abbrev Lean.Lsp.ProgressToken : Type

Reference to the progress of some in-flight piece of work.

reference

structure Lean.Lsp.ProgressParams (α : Type) : Type

Params for JSON-RPC method $/progress request.

reference

• token : ProgressToken
• value : α

instance Lean.Lsp.instToJsonProgressParams {α✝ : Type} [ToJson α✝] : ToJson (ProgressParams α✝)

structure Lean.Lsp.WorkDoneProgressReport : Type

• kind : String
• message? : Option String

  More detailed associated progress message.

• cancellable : Bool

  Controls if a cancel button should show to allow the user to cancel the operation.

• percentage? : Option Nat

  Optional progress percentage to display (value 100 is considered 100%). If not provided infinite progress is assumed.

instance Lean.Lsp.instToJsonWorkDoneProgressReport : ToJson WorkDoneProgressReport

structure Lean.Lsp.WorkDoneProgressBeginextends Lean.Lsp.WorkDoneProgressReport : Type

Notification to signal the start of progress reporting.

• kind : String
• message? : Option String
• cancellable : Bool
• percentage? : Option Nat
• title : String

instance Lean.Lsp.instToJsonWorkDoneProgressBegin : ToJson WorkDoneProgressBegin

structure Lean.Lsp.WorkDoneProgressEnd : Type

Signals the end of progress reporting.

• kind : String
• message? : Option String

instance Lean.Lsp.instToJsonWorkDoneProgressEnd : ToJson WorkDoneProgressEnd

structure Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option ProgressToken

instance Lean.Lsp.instToJsonWorkDoneProgressParams : ToJson WorkDoneProgressParams

instance Lean.Lsp.instFromJsonWorkDoneProgressParams : FromJson WorkDoneProgressParams

structure Lean.Lsp.PartialResultParams : Type

• partialResultToken? : Option ProgressToken

instance Lean.Lsp.instToJsonPartialResultParams : ToJson PartialResultParams

instance Lean.Lsp.instFromJsonPartialResultParams : FromJson PartialResultParams

structure Lean.Lsp.WorkDoneProgressOptions : Type

reference

• workDoneProgress : Bool

instance Lean.Lsp.instToJsonWorkDoneProgressOptions : ToJson WorkDoneProgressOptions

instance Lean.Lsp.instFromJsonWorkDoneProgressOptions : FromJson WorkDoneProgressOptions

structure Lean.Lsp.ResolveSupport : Type

• properties : Array String

instance Lean.Lsp.instFromJsonResolveSupport : FromJson ResolveSupport

instance Lean.Lsp.instToJsonResolveSupport : ToJson ResolveSupport