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 : Lean.JsonRpc.RequestID

instance Lean.Lsp.instInhabitedCancelParams : Inhabited Lean.Lsp.CancelParams

instance Lean.Lsp.instBEqCancelParams : BEq Lean.Lsp.CancelParams

instance Lean.Lsp.instToJsonCancelParams : Lean.ToJson Lean.Lsp.CancelParams

instance Lean.Lsp.instFromJsonCancelParams : Lean.FromJson Lean.Lsp.CancelParams

@[inline, reducible]

abbrev Lean.Lsp.DocumentUri : Type

structure Lean.Lsp.Position : Type

• line : Nat
• character : Nat

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)

instance Lean.Lsp.instInhabitedPosition : Inhabited Lean.Lsp.Position

instance Lean.Lsp.instBEqPosition : BEq Lean.Lsp.Position

instance Lean.Lsp.instOrdPosition : Ord Lean.Lsp.Position

instance Lean.Lsp.instHashablePosition : Hashable Lean.Lsp.Position

instance Lean.Lsp.instToJsonPosition : Lean.ToJson Lean.Lsp.Position

instance Lean.Lsp.instFromJsonPosition : Lean.FromJson Lean.Lsp.Position

instance Lean.Lsp.instToStringPosition : ToString Lean.Lsp.Position

instance Lean.Lsp.instLTPosition : LT Lean.Lsp.Position

instance Lean.Lsp.instLEPosition : LE Lean.Lsp.Position

structure Lean.Lsp.Range : Type

• start : Lean.Lsp.Position
• end : Lean.Lsp.Position

instance Lean.Lsp.instInhabitedRange : Inhabited Lean.Lsp.Range

instance Lean.Lsp.instBEqRange : BEq Lean.Lsp.Range

instance Lean.Lsp.instHashableRange : Hashable Lean.Lsp.Range

instance Lean.Lsp.instToJsonRange : Lean.ToJson Lean.Lsp.Range

instance Lean.Lsp.instFromJsonRange : Lean.FromJson Lean.Lsp.Range

instance Lean.Lsp.instOrdRange : Ord Lean.Lsp.Range

instance Lean.Lsp.instLTRange : LT Lean.Lsp.Range

instance Lean.Lsp.instLERange : LE Lean.Lsp.Range

structure Lean.Lsp.Location : Type

• uri : Lean.Lsp.DocumentUri
• range : Lean.Lsp.Range

A Location is a DocumentUri and a Range.

instance Lean.Lsp.instInhabitedLocation : Inhabited Lean.Lsp.Location

instance Lean.Lsp.instBEqLocation : BEq Lean.Lsp.Location

instance Lean.Lsp.instToJsonLocation : Lean.ToJson Lean.Lsp.Location

instance Lean.Lsp.instFromJsonLocation : Lean.FromJson Lean.Lsp.Location

structure Lean.Lsp.LocationLink : Type

• originSelectionRange? : Option Lean.Lsp.Range
• targetUri : Lean.Lsp.DocumentUri
• targetRange : Lean.Lsp.Range
• targetSelectionRange : Lean.Lsp.Range

instance Lean.Lsp.instToJsonLocationLink : Lean.ToJson Lean.Lsp.LocationLink

instance Lean.Lsp.instFromJsonLocationLink : Lean.FromJson Lean.Lsp.LocationLink

structure Lean.Lsp.Command : Type

• title : String

  Title of the command, like save.

• command : String

  The identifier of the actual command handler.

• arguments? : Option (Array Lean.Json)

  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.

reference

instance Lean.Lsp.instToJsonCommand : Lean.ToJson Lean.Lsp.Command

instance Lean.Lsp.instFromJsonCommand : Lean.FromJson Lean.Lsp.Command

structure Lean.Lsp.TextEdit : Type

• range : Lean.Lsp.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.

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

A textual edit applicable to a text document.

reference

instance Lean.Lsp.instToJsonTextEdit : Lean.ToJson Lean.Lsp.TextEdit

instance Lean.Lsp.instFromJsonTextEdit : Lean.FromJson Lean.Lsp.TextEdit

def Lean.Lsp.TextEditBatch : Type

An array of TextEdits to be performed in sequence.

instance Lean.Lsp.instFromJsonTextEditBatch : Lean.FromJson Lean.Lsp.TextEditBatch

instance Lean.Lsp.instToJsonTextEditBatch : Lean.ToJson Lean.Lsp.TextEditBatch

instance Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection Lean.Lsp.TextEditBatch

instance Lean.Lsp.instAppendTextEditBatch : Append Lean.Lsp.TextEditBatch

instance Lean.Lsp.instCoeTextEditTextEditBatch : Coe Lean.Lsp.TextEdit Lean.Lsp.TextEditBatch

structure Lean.Lsp.TextDocumentIdentifier : Type

• uri : Lean.Lsp.DocumentUri

instance Lean.Lsp.instToJsonTextDocumentIdentifier : Lean.ToJson Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instFromJsonTextDocumentIdentifier : Lean.FromJson Lean.Lsp.TextDocumentIdentifier

structure Lean.Lsp.VersionedTextDocumentIdentifier : Type

• uri : Lean.Lsp.DocumentUri
• version? : Option Nat

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : Lean.ToJson Lean.Lsp.VersionedTextDocumentIdentifier

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : Lean.FromJson Lean.Lsp.VersionedTextDocumentIdentifier

structure Lean.Lsp.TextDocumentEdit : Type

• textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
• edits : Lean.Lsp.TextEditBatch

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

reference

instance Lean.Lsp.instToJsonTextDocumentEdit : Lean.ToJson Lean.Lsp.TextDocumentEdit

instance Lean.Lsp.instFromJsonTextDocumentEdit : Lean.FromJson Lean.Lsp.TextDocumentEdit

structure Lean.Lsp.ChangeAnnotation : Type

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

Additional information that describes document changes.

reference

instance Lean.Lsp.instToJsonChangeAnnotation : Lean.ToJson Lean.Lsp.ChangeAnnotation

instance Lean.Lsp.instFromJsonChangeAnnotation : Lean.FromJson Lean.Lsp.ChangeAnnotation

structure Lean.Lsp.CreateFile.Options : Type

• overwrite : Bool
• ignoreIfExists : Bool

Options for CreateFile and RenameFile.

instance Lean.Lsp.CreateFile.instToJsonOptions : Lean.ToJson Lean.Lsp.CreateFile.Options

instance Lean.Lsp.CreateFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.CreateFile.Options

structure Lean.Lsp.DeleteFile.Options : Type

• recursive : Bool
• ignoreIfNotExists : Bool

Options for DeleteFile.

instance Lean.Lsp.DeleteFile.instToJsonOptions : Lean.ToJson Lean.Lsp.DeleteFile.Options

instance Lean.Lsp.DeleteFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.DeleteFile.Options

structure Lean.Lsp.CreateFile : Type

• uri : Lean.Lsp.DocumentUri
• options? : Option Lean.Lsp.CreateFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonCreateFile : Lean.ToJson Lean.Lsp.CreateFile

instance Lean.Lsp.instFromJsonCreateFile : Lean.FromJson Lean.Lsp.CreateFile

structure Lean.Lsp.RenameFile : Type

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

instance Lean.Lsp.instToJsonRenameFile : Lean.ToJson Lean.Lsp.RenameFile

instance Lean.Lsp.instFromJsonRenameFile : Lean.FromJson Lean.Lsp.RenameFile

structure Lean.Lsp.DeleteFile : Type

• uri : Lean.Lsp.DocumentUri
• options? : Option Lean.Lsp.DeleteFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonDeleteFile : Lean.ToJson Lean.Lsp.DeleteFile

instance Lean.Lsp.instFromJsonDeleteFile : Lean.FromJson Lean.Lsp.DeleteFile

inductive Lean.Lsp.DocumentChange : Type

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

reference

instance Lean.Lsp.instToJsonDocumentChange : Lean.ToJson Lean.Lsp.DocumentChange

instance Lean.Lsp.instFromJsonDocumentChange : Lean.FromJson Lean.Lsp.DocumentChange

structure Lean.Lsp.WorkspaceEdit : Type

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

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

reference

instance Lean.Lsp.instToJsonWorkspaceEdit : Lean.ToJson Lean.Lsp.WorkspaceEdit

instance Lean.Lsp.instFromJsonWorkspaceEdit : Lean.FromJson Lean.Lsp.WorkspaceEdit

instance Lean.Lsp.WorkspaceEdit.instEmptyCollectionWorkspaceEdit : EmptyCollection Lean.Lsp.WorkspaceEdit

instance Lean.Lsp.WorkspaceEdit.instAppendWorkspaceEdit : Append Lean.Lsp.WorkspaceEdit

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

def Lean.Lsp.WorkspaceEdit.ofTextEdit (uri : Lean.Lsp.DocumentUri) (te : Lean.Lsp.TextEdit) : Lean.Lsp.WorkspaceEdit

structure Lean.Lsp.ApplyWorkspaceEditParams : Type

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

reference

instance Lean.Lsp.instToJsonApplyWorkspaceEditParams : Lean.ToJson Lean.Lsp.ApplyWorkspaceEditParams

instance Lean.Lsp.instFromJsonApplyWorkspaceEditParams : Lean.FromJson Lean.Lsp.ApplyWorkspaceEditParams

structure Lean.Lsp.TextDocumentItem : Type

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

reference

instance Lean.Lsp.instToJsonTextDocumentItem : Lean.ToJson Lean.Lsp.TextDocumentItem

instance Lean.Lsp.instFromJsonTextDocumentItem : Lean.FromJson Lean.Lsp.TextDocumentItem

structure Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier
• position : Lean.Lsp.Position

instance Lean.Lsp.instToJsonTextDocumentPositionParams : Lean.ToJson Lean.Lsp.TextDocumentPositionParams

instance Lean.Lsp.instFromJsonTextDocumentPositionParams : Lean.FromJson Lean.Lsp.TextDocumentPositionParams

instance Lean.Lsp.instToStringTextDocumentPositionParams : ToString Lean.Lsp.TextDocumentPositionParams

structure Lean.Lsp.DocumentFilter : Type

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

instance Lean.Lsp.instToJsonDocumentFilter : Lean.ToJson Lean.Lsp.DocumentFilter

instance Lean.Lsp.instFromJsonDocumentFilter : Lean.FromJson Lean.Lsp.DocumentFilter

def Lean.Lsp.DocumentSelector : Type

instance Lean.Lsp.instFromJsonDocumentSelector : Lean.FromJson Lean.Lsp.DocumentSelector

instance Lean.Lsp.instToJsonDocumentSelector : Lean.ToJson Lean.Lsp.DocumentSelector

structure Lean.Lsp.StaticRegistrationOptions : Type

• id? : Option String

instance Lean.Lsp.instToJsonStaticRegistrationOptions : Lean.ToJson Lean.Lsp.StaticRegistrationOptions

instance Lean.Lsp.instFromJsonStaticRegistrationOptions : Lean.FromJson Lean.Lsp.StaticRegistrationOptions

structure Lean.Lsp.TextDocumentRegistrationOptions : Type

• documentSelector? : Option Lean.Lsp.DocumentSelector

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions : Lean.ToJson Lean.Lsp.TextDocumentRegistrationOptions

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : Lean.FromJson Lean.Lsp.TextDocumentRegistrationOptions

inductive Lean.Lsp.MarkupKind : Type

• plaintext: Lean.Lsp.MarkupKind
• markdown: Lean.Lsp.MarkupKind

instance Lean.Lsp.instFromJsonMarkupKind : Lean.FromJson Lean.Lsp.MarkupKind

instance Lean.Lsp.instToJsonMarkupKind : Lean.ToJson Lean.Lsp.MarkupKind

structure Lean.Lsp.MarkupContent : Type

• kind : Lean.Lsp.MarkupKind
• value : String

instance Lean.Lsp.instToJsonMarkupContent : Lean.ToJson Lean.Lsp.MarkupContent

instance Lean.Lsp.instFromJsonMarkupContent : Lean.FromJson Lean.Lsp.MarkupContent

@[inline, reducible]

abbrev Lean.Lsp.ProgressToken : Type

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

reference

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

• token : Lean.Lsp.ProgressToken
• value : α

Params for JSON-RPC method $/progress request.

reference

instance Lean.Lsp.instToJsonProgressParams : {α : Type} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Lsp.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 : Lean.ToJson Lean.Lsp.WorkDoneProgressReport

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

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

Notification to signal the start of progress reporting.

instance Lean.Lsp.instToJsonWorkDoneProgressBegin : Lean.ToJson Lean.Lsp.WorkDoneProgressBegin

structure Lean.Lsp.WorkDoneProgressEnd : Type

• kind : String
• message? : Option String

Signals the end of progress reporting.

instance Lean.Lsp.instToJsonWorkDoneProgressEnd : Lean.ToJson Lean.Lsp.WorkDoneProgressEnd

structure Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option Lean.Lsp.ProgressToken

instance Lean.Lsp.instToJsonWorkDoneProgressParams : Lean.ToJson Lean.Lsp.WorkDoneProgressParams

instance Lean.Lsp.instFromJsonWorkDoneProgressParams : Lean.FromJson Lean.Lsp.WorkDoneProgressParams

structure Lean.Lsp.PartialResultParams : Type

• partialResultToken? : Option Lean.Lsp.ProgressToken

instance Lean.Lsp.instToJsonPartialResultParams : Lean.ToJson Lean.Lsp.PartialResultParams

instance Lean.Lsp.instFromJsonPartialResultParams : Lean.FromJson Lean.Lsp.PartialResultParams

structure Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool

reference

instance Lean.Lsp.instToJsonWorkDoneProgressOptions : Lean.ToJson Lean.Lsp.WorkDoneProgressOptions

instance Lean.Lsp.instFromJsonWorkDoneProgressOptions : Lean.FromJson Lean.Lsp.WorkDoneProgressOptions