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.

structure Lean.Lsp.CancelParams : Type

• id : JsonRpc.RequestID

instance Lean.Lsp.instInhabitedCancelParams : Inhabited CancelParams

Equations

• Lean.Lsp.instInhabitedCancelParams = { default := { id := default } }

instance Lean.Lsp.instBEqCancelParams : BEq CancelParams

Equations

• Lean.Lsp.instBEqCancelParams = { beq := Lean.Lsp.beqCancelParams✝ }

instance Lean.Lsp.instToJsonCancelParams : ToJson CancelParams

Equations

• Lean.Lsp.instToJsonCancelParams = { toJson := Lean.Lsp.toJsonCancelParams✝ }

instance Lean.Lsp.instFromJsonCancelParams : FromJson CancelParams

Equations

• Lean.Lsp.instFromJsonCancelParams = { fromJson? := Lean.Lsp.fromJsonCancelParams✝ }

@[reducible, inline]

abbrev Lean.Lsp.DocumentUri : Type

Equations

• Lean.Lsp.DocumentUri = String

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

Equations

• Lean.Lsp.instInhabitedPosition = { default := { line := default, character := default } }

instance Lean.Lsp.instBEqPosition : BEq Position

Equations

• Lean.Lsp.instBEqPosition = { beq := Lean.Lsp.beqPosition✝ }

instance Lean.Lsp.instOrdPosition : Ord Position

Equations

• Lean.Lsp.instOrdPosition = { compare := Lean.Lsp.ordPosition✝ }

instance Lean.Lsp.instHashablePosition : Hashable Position

Equations

• Lean.Lsp.instHashablePosition = { hash := Lean.Lsp.hashPosition✝ }

instance Lean.Lsp.instToJsonPosition : ToJson Position

Equations

• Lean.Lsp.instToJsonPosition = { toJson := Lean.Lsp.toJsonPosition✝ }

instance Lean.Lsp.instFromJsonPosition : FromJson Position

Equations

• Lean.Lsp.instFromJsonPosition = { fromJson? := Lean.Lsp.fromJsonPosition✝ }

instance Lean.Lsp.instToStringPosition : ToString Position

Equations

• Lean.Lsp.instToStringPosition = { toString := fun (p : Lean.Lsp.Position) => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")" }

instance Lean.Lsp.instLTPosition : LT Position

Equations

• Lean.Lsp.instLTPosition = ltOfOrd

instance Lean.Lsp.instLEPosition : LE Position

Equations

• Lean.Lsp.instLEPosition = leOfOrd

structure Lean.Lsp.Range : Type

• start : Position
• end : Position

instance Lean.Lsp.instInhabitedRange : Inhabited Range

Equations

• Lean.Lsp.instInhabitedRange = { default := { start := default, «end» := default } }

instance Lean.Lsp.instBEqRange : BEq Range

Equations

• Lean.Lsp.instBEqRange = { beq := Lean.Lsp.beqRange✝ }

instance Lean.Lsp.instHashableRange : Hashable Range

Equations

• Lean.Lsp.instHashableRange = { hash := Lean.Lsp.hashRange✝ }

instance Lean.Lsp.instToJsonRange : ToJson Range

Equations

• Lean.Lsp.instToJsonRange = { toJson := Lean.Lsp.toJsonRange✝ }

instance Lean.Lsp.instFromJsonRange : FromJson Range

Equations

• Lean.Lsp.instFromJsonRange = { fromJson? := Lean.Lsp.fromJsonRange✝ }

instance Lean.Lsp.instOrdRange : Ord Range

Equations

• Lean.Lsp.instOrdRange = { compare := Lean.Lsp.ordRange✝ }

instance Lean.Lsp.instLTRange : LT Range

Equations

• Lean.Lsp.instLTRange = ltOfOrd

instance Lean.Lsp.instLERange : LE Range

Equations

• Lean.Lsp.instLERange = leOfOrd

structure Lean.Lsp.Location : Type

A Location is a DocumentUri and a Range.

• uri : DocumentUri
• range : Range

instance Lean.Lsp.instInhabitedLocation : Inhabited Location

Equations

• Lean.Lsp.instInhabitedLocation = { default := { uri := default, range := default } }

instance Lean.Lsp.instBEqLocation : BEq Location

Equations

• Lean.Lsp.instBEqLocation = { beq := Lean.Lsp.beqLocation✝ }

instance Lean.Lsp.instToJsonLocation : ToJson Location

Equations

• Lean.Lsp.instToJsonLocation = { toJson := Lean.Lsp.toJsonLocation✝ }

instance Lean.Lsp.instFromJsonLocation : FromJson Location

Equations

• Lean.Lsp.instFromJsonLocation = { fromJson? := Lean.Lsp.fromJsonLocation✝ }

instance Lean.Lsp.instOrdLocation : Ord Location

Equations

• Lean.Lsp.instOrdLocation = { compare := Lean.Lsp.ordLocation✝ }

structure Lean.Lsp.LocationLink : Type

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

instance Lean.Lsp.instToJsonLocationLink : ToJson LocationLink

Equations

• Lean.Lsp.instToJsonLocationLink = { toJson := Lean.Lsp.toJsonLocationLink✝ }

instance Lean.Lsp.instFromJsonLocationLink : FromJson LocationLink

Equations

• Lean.Lsp.instFromJsonLocationLink = { fromJson? := Lean.Lsp.fromJsonLocationLink✝ }

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

Equations

• Lean.Lsp.instToJsonCommand = { toJson := Lean.Lsp.toJsonCommand✝ }

instance Lean.Lsp.instFromJsonCommand : FromJson Command

Equations

• Lean.Lsp.instFromJsonCommand = { fromJson? := Lean.Lsp.fromJsonCommand✝ }

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

Equations

• Lean.Lsp.instToJsonSnippetString = { toJson := Lean.Lsp.toJsonSnippetString✝ }

instance Lean.Lsp.instFromJsonSnippetString : FromJson SnippetString

Equations

• Lean.Lsp.instFromJsonSnippetString = { fromJson? := Lean.Lsp.fromJsonSnippetString✝ }

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

Equations

• Lean.Lsp.instToJsonTextEdit = { toJson := Lean.Lsp.toJsonTextEdit✝ }

instance Lean.Lsp.instFromJsonTextEdit : FromJson TextEdit

Equations

• Lean.Lsp.instFromJsonTextEdit = { fromJson? := Lean.Lsp.fromJsonTextEdit✝ }

def Lean.Lsp.TextEditBatch : Type

An array of TextEdits to be performed in sequence.

Equations

• Lean.Lsp.TextEditBatch = Array Lean.Lsp.TextEdit

instance Lean.Lsp.instFromJsonTextEditBatch : FromJson TextEditBatch

Equations

• Lean.Lsp.instFromJsonTextEditBatch = { fromJson? := Lean.fromJson? }

instance Lean.Lsp.instToJsonTextEditBatch : ToJson TextEditBatch

Equations

• Lean.Lsp.instToJsonTextEditBatch = { toJson := Lean.toJson }

instance Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection TextEditBatch

Equations

• Lean.Lsp.instEmptyCollectionTextEditBatch = { emptyCollection := #[] }

instance Lean.Lsp.instAppendTextEditBatch : Append TextEditBatch

Equations

• Lean.Lsp.instAppendTextEditBatch = inferInstanceAs (Append (Array Lean.Lsp.TextEdit))

instance Lean.Lsp.instCoeTextEditTextEditBatch : Coe TextEdit TextEditBatch

Equations

• Lean.Lsp.instCoeTextEditTextEditBatch = { coe := fun (te : Lean.Lsp.TextEdit) => #[te] }

structure Lean.Lsp.TextDocumentIdentifier : Type

• uri : DocumentUri

instance Lean.Lsp.instToJsonTextDocumentIdentifier : ToJson TextDocumentIdentifier

Equations

• Lean.Lsp.instToJsonTextDocumentIdentifier = { toJson := Lean.Lsp.toJsonTextDocumentIdentifier✝ }

instance Lean.Lsp.instFromJsonTextDocumentIdentifier : FromJson TextDocumentIdentifier

Equations

• Lean.Lsp.instFromJsonTextDocumentIdentifier = { fromJson? := Lean.Lsp.fromJsonTextDocumentIdentifier✝ }

structure Lean.Lsp.VersionedTextDocumentIdentifier : Type

• uri : DocumentUri
• version? : Option Nat

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : ToJson VersionedTextDocumentIdentifier

Equations

• Lean.Lsp.instToJsonVersionedTextDocumentIdentifier = { toJson := Lean.Lsp.toJsonVersionedTextDocumentIdentifier✝ }

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : FromJson VersionedTextDocumentIdentifier

Equations

• Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier = { fromJson? := Lean.Lsp.fromJsonVersionedTextDocumentIdentifier✝ }

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

Equations

• Lean.Lsp.instToJsonTextDocumentEdit = { toJson := Lean.Lsp.toJsonTextDocumentEdit✝ }

instance Lean.Lsp.instFromJsonTextDocumentEdit : FromJson TextDocumentEdit

Equations

• Lean.Lsp.instFromJsonTextDocumentEdit = { fromJson? := Lean.Lsp.fromJsonTextDocumentEdit✝ }

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

Equations

• Lean.Lsp.instToJsonChangeAnnotation = { toJson := Lean.Lsp.toJsonChangeAnnotation✝ }

instance Lean.Lsp.instFromJsonChangeAnnotation : FromJson ChangeAnnotation

Equations

• Lean.Lsp.instFromJsonChangeAnnotation = { fromJson? := Lean.Lsp.fromJsonChangeAnnotation✝ }

structure Lean.Lsp.CreateFile.Options : Type

Options for CreateFile and RenameFile.

• overwrite : Bool
• ignoreIfExists : Bool

instance Lean.Lsp.CreateFile.instToJsonOptions : ToJson Options

Equations

• Lean.Lsp.CreateFile.instToJsonOptions = { toJson := Lean.Lsp.CreateFile.toJsonOptions✝ }

instance Lean.Lsp.CreateFile.instFromJsonOptions : FromJson Options

Equations

• Lean.Lsp.CreateFile.instFromJsonOptions = { fromJson? := Lean.Lsp.CreateFile.fromJsonOptions✝ }

structure Lean.Lsp.DeleteFile.Options : Type

Options for DeleteFile.

• recursive : Bool
• ignoreIfNotExists : Bool

instance Lean.Lsp.DeleteFile.instToJsonOptions : ToJson Options

Equations

• Lean.Lsp.DeleteFile.instToJsonOptions = { toJson := Lean.Lsp.DeleteFile.toJsonOptions✝ }

instance Lean.Lsp.DeleteFile.instFromJsonOptions : FromJson Options

Equations

• Lean.Lsp.DeleteFile.instFromJsonOptions = { fromJson? := Lean.Lsp.DeleteFile.fromJsonOptions✝ }

structure Lean.Lsp.CreateFile : Type

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

instance Lean.Lsp.instToJsonCreateFile : ToJson CreateFile

Equations

• Lean.Lsp.instToJsonCreateFile = { toJson := Lean.Lsp.toJsonCreateFile✝ }

instance Lean.Lsp.instFromJsonCreateFile : FromJson CreateFile

Equations

• Lean.Lsp.instFromJsonCreateFile = { fromJson? := Lean.Lsp.fromJsonCreateFile✝ }

structure Lean.Lsp.RenameFile : Type

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

instance Lean.Lsp.instToJsonRenameFile : ToJson RenameFile

Equations

• Lean.Lsp.instToJsonRenameFile = { toJson := Lean.Lsp.toJsonRenameFile✝ }

instance Lean.Lsp.instFromJsonRenameFile : FromJson RenameFile

Equations

• Lean.Lsp.instFromJsonRenameFile = { fromJson? := Lean.Lsp.fromJsonRenameFile✝ }

structure Lean.Lsp.DeleteFile : Type

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

instance Lean.Lsp.instToJsonDeleteFile : ToJson DeleteFile

Equations

• Lean.Lsp.instToJsonDeleteFile = { toJson := Lean.Lsp.toJsonDeleteFile✝ }

instance Lean.Lsp.instFromJsonDeleteFile : FromJson DeleteFile

Equations

• Lean.Lsp.instFromJsonDeleteFile = { fromJson? := Lean.Lsp.fromJsonDeleteFile✝ }

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instFromJsonDocumentChange : FromJson DocumentChange

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Lsp.instToJsonWorkspaceEdit = { toJson := Lean.Lsp.toJsonWorkspaceEdit✝ }

instance Lean.Lsp.instFromJsonWorkspaceEdit : FromJson WorkspaceEdit

Equations

• Lean.Lsp.instFromJsonWorkspaceEdit = { fromJson? := Lean.Lsp.fromJsonWorkspaceEdit✝ }

instance Lean.Lsp.WorkspaceEdit.instEmptyCollection : EmptyCollection WorkspaceEdit

Equations

• Lean.Lsp.WorkspaceEdit.instEmptyCollection = { emptyCollection := { changes? := none, documentChanges? := none, changeAnnotations? := none } }

instance Lean.Lsp.WorkspaceEdit.instAppend : Append WorkspaceEdit

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit e = { changes? := none, documentChanges? := some #[Lean.Lsp.DocumentChange.edit e], changeAnnotations? := none }

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

Equations

• Lean.Lsp.WorkspaceEdit.ofTextEdit doc te = Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit { textDocument := doc, edits := #[te] }

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

Equations

• Lean.Lsp.instToJsonApplyWorkspaceEditParams = { toJson := Lean.Lsp.toJsonApplyWorkspaceEditParams✝ }

instance Lean.Lsp.instFromJsonApplyWorkspaceEditParams : FromJson ApplyWorkspaceEditParams

Equations

• Lean.Lsp.instFromJsonApplyWorkspaceEditParams = { fromJson? := Lean.Lsp.fromJsonApplyWorkspaceEditParams✝ }

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

Equations

• Lean.Lsp.instToJsonTextDocumentItem = { toJson := Lean.Lsp.toJsonTextDocumentItem✝ }

instance Lean.Lsp.instFromJsonTextDocumentItem : FromJson TextDocumentItem

Equations

• Lean.Lsp.instFromJsonTextDocumentItem = { fromJson? := Lean.Lsp.fromJsonTextDocumentItem✝ }

structure Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instToJsonTextDocumentPositionParams : ToJson TextDocumentPositionParams

Equations

• Lean.Lsp.instToJsonTextDocumentPositionParams = { toJson := Lean.Lsp.toJsonTextDocumentPositionParams✝ }

instance Lean.Lsp.instFromJsonTextDocumentPositionParams : FromJson TextDocumentPositionParams

Equations

• Lean.Lsp.instFromJsonTextDocumentPositionParams = { fromJson? := Lean.Lsp.fromJsonTextDocumentPositionParams✝ }

instance Lean.Lsp.instToStringTextDocumentPositionParams : ToString TextDocumentPositionParams

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Lsp.DocumentFilter : Type

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

instance Lean.Lsp.instToJsonDocumentFilter : ToJson DocumentFilter

Equations

• Lean.Lsp.instToJsonDocumentFilter = { toJson := Lean.Lsp.toJsonDocumentFilter✝ }

instance Lean.Lsp.instFromJsonDocumentFilter : FromJson DocumentFilter

Equations

• Lean.Lsp.instFromJsonDocumentFilter = { fromJson? := Lean.Lsp.fromJsonDocumentFilter✝ }

def Lean.Lsp.DocumentSelector : Type

Equations

• Lean.Lsp.DocumentSelector = Array Lean.Lsp.DocumentFilter

instance Lean.Lsp.instFromJsonDocumentSelector : FromJson DocumentSelector

Equations

• Lean.Lsp.instFromJsonDocumentSelector = { fromJson? := Lean.fromJson? }

instance Lean.Lsp.instToJsonDocumentSelector : ToJson DocumentSelector

Equations

• Lean.Lsp.instToJsonDocumentSelector = { toJson := Lean.toJson }

structure Lean.Lsp.StaticRegistrationOptions : Type

• id? : Option String

instance Lean.Lsp.instToJsonStaticRegistrationOptions : ToJson StaticRegistrationOptions

Equations

• Lean.Lsp.instToJsonStaticRegistrationOptions = { toJson := Lean.Lsp.toJsonStaticRegistrationOptions✝ }

instance Lean.Lsp.instFromJsonStaticRegistrationOptions : FromJson StaticRegistrationOptions

Equations

• Lean.Lsp.instFromJsonStaticRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonStaticRegistrationOptions✝ }

structure Lean.Lsp.TextDocumentRegistrationOptions : Type

• documentSelector? : Option DocumentSelector

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions : ToJson TextDocumentRegistrationOptions

Equations

• Lean.Lsp.instToJsonTextDocumentRegistrationOptions = { toJson := Lean.Lsp.toJsonTextDocumentRegistrationOptions✝ }

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : FromJson TextDocumentRegistrationOptions

Equations

• Lean.Lsp.instFromJsonTextDocumentRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonTextDocumentRegistrationOptions✝ }

inductive Lean.Lsp.MarkupKind : Type

• plaintext : MarkupKind
• markdown : MarkupKind

instance Lean.Lsp.instDecidableEqMarkupKind : DecidableEq MarkupKind

Equations

• Lean.Lsp.instDecidableEqMarkupKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Lsp.instHashableMarkupKind : Hashable MarkupKind

Equations

• Lean.Lsp.instHashableMarkupKind = { hash := Lean.Lsp.hashMarkupKind✝ }

instance Lean.Lsp.instFromJsonMarkupKind : FromJson MarkupKind

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instToJsonMarkupKind : ToJson MarkupKind

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Lsp.MarkupContent : Type

• kind : MarkupKind
• value : String

instance Lean.Lsp.instToJsonMarkupContent : ToJson MarkupContent

Equations

• Lean.Lsp.instToJsonMarkupContent = { toJson := Lean.Lsp.toJsonMarkupContent✝ }

instance Lean.Lsp.instFromJsonMarkupContent : FromJson MarkupContent

Equations

• Lean.Lsp.instFromJsonMarkupContent = { fromJson? := Lean.Lsp.fromJsonMarkupContent✝ }

instance Lean.Lsp.instDecidableEqMarkupContent : DecidableEq MarkupContent

Equations

• Lean.Lsp.instDecidableEqMarkupContent = Lean.Lsp.decEqMarkupContent✝

instance Lean.Lsp.instHashableMarkupContent : Hashable MarkupContent

Equations

• Lean.Lsp.instHashableMarkupContent = { hash := Lean.Lsp.hashMarkupContent✝ }

@[reducible, inline]

abbrev Lean.Lsp.ProgressToken : Type

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

reference

Equations

• Lean.Lsp.ProgressToken = String

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 α✝)

Equations

• Lean.Lsp.instToJsonProgressParams = { toJson := Lean.Lsp.toJsonProgressParams✝ }

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

Equations

• Lean.Lsp.instToJsonWorkDoneProgressReport = { toJson := Lean.Lsp.toJsonWorkDoneProgressReport✝ }

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

Equations

• Lean.Lsp.instToJsonWorkDoneProgressBegin = { toJson := Lean.Lsp.toJsonWorkDoneProgressBegin✝ }

structure Lean.Lsp.WorkDoneProgressEnd : Type

Signals the end of progress reporting.

• kind : String
• message? : Option String

instance Lean.Lsp.instToJsonWorkDoneProgressEnd : ToJson WorkDoneProgressEnd

Equations

• Lean.Lsp.instToJsonWorkDoneProgressEnd = { toJson := Lean.Lsp.toJsonWorkDoneProgressEnd✝ }

structure Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option ProgressToken

instance Lean.Lsp.instToJsonWorkDoneProgressParams : ToJson WorkDoneProgressParams

Equations

• Lean.Lsp.instToJsonWorkDoneProgressParams = { toJson := Lean.Lsp.toJsonWorkDoneProgressParams✝ }

instance Lean.Lsp.instFromJsonWorkDoneProgressParams : FromJson WorkDoneProgressParams

Equations

• Lean.Lsp.instFromJsonWorkDoneProgressParams = { fromJson? := Lean.Lsp.fromJsonWorkDoneProgressParams✝ }

structure Lean.Lsp.PartialResultParams : Type

• partialResultToken? : Option ProgressToken

instance Lean.Lsp.instToJsonPartialResultParams : ToJson PartialResultParams

Equations

• Lean.Lsp.instToJsonPartialResultParams = { toJson := Lean.Lsp.toJsonPartialResultParams✝ }

instance Lean.Lsp.instFromJsonPartialResultParams : FromJson PartialResultParams

Equations

• Lean.Lsp.instFromJsonPartialResultParams = { fromJson? := Lean.Lsp.fromJsonPartialResultParams✝ }

structure Lean.Lsp.WorkDoneProgressOptions : Type

reference

• workDoneProgress : Bool

instance Lean.Lsp.instToJsonWorkDoneProgressOptions : ToJson WorkDoneProgressOptions

Equations

• Lean.Lsp.instToJsonWorkDoneProgressOptions = { toJson := Lean.Lsp.toJsonWorkDoneProgressOptions✝ }

instance Lean.Lsp.instFromJsonWorkDoneProgressOptions : FromJson WorkDoneProgressOptions

Equations

• Lean.Lsp.instFromJsonWorkDoneProgressOptions = { fromJson? := Lean.Lsp.fromJsonWorkDoneProgressOptions✝ }