Documentation

Lean.Data.Lsp.Basic

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

Equations

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

instance Lean.Lsp.instBEqCancelParams:

BEq Lean.Lsp.CancelParams

Equations

Lean.Lsp.instBEqCancelParams = { beq := [anonymous] }

instance Lean.Lsp.instToJsonCancelParams:

Lean.ToJson Lean.Lsp.CancelParams

Equations

Lean.Lsp.instToJsonCancelParams = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonCancelParams:

Lean.FromJson Lean.Lsp.CancelParams

Equations

Lean.Lsp.instFromJsonCancelParams = { fromJson? := [anonymous] }

@[inline]

abbrev Lean.Lsp.DocumentUri:

Type

Equations

Lean.Lsp.DocumentUri = String

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

Equations

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

instance Lean.Lsp.instBEqPosition:

BEq Lean.Lsp.Position

Equations

Lean.Lsp.instBEqPosition = { beq := [anonymous] }

instance Lean.Lsp.instOrdPosition:

Ord Lean.Lsp.Position

Equations

Lean.Lsp.instOrdPosition = { compare := [anonymous] }

instance Lean.Lsp.instHashablePosition:

Hashable Lean.Lsp.Position

Equations

Lean.Lsp.instHashablePosition = { hash := [anonymous] }

instance Lean.Lsp.instToJsonPosition:

Lean.ToJson Lean.Lsp.Position

Equations

Lean.Lsp.instToJsonPosition = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonPosition:

Lean.FromJson Lean.Lsp.Position

Equations

Lean.Lsp.instFromJsonPosition = { fromJson? := [anonymous] }

instance Lean.Lsp.instToStringPosition:

ToString Lean.Lsp.Position

Equations

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

instance Lean.Lsp.instLTPosition:

LT Lean.Lsp.Position

Equations

Lean.Lsp.instLTPosition = ltOfOrd

instance Lean.Lsp.instLEPosition:

LE Lean.Lsp.Position

Equations

Lean.Lsp.instLEPosition = leOfOrd

structure Lean.Lsp.Range:

Type

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

instance Lean.Lsp.instInhabitedRange:

Inhabited Lean.Lsp.Range

Equations

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

instance Lean.Lsp.instBEqRange:

BEq Lean.Lsp.Range

Equations

Lean.Lsp.instBEqRange = { beq := [anonymous] }

instance Lean.Lsp.instHashableRange:

Hashable Lean.Lsp.Range

Equations

Lean.Lsp.instHashableRange = { hash := [anonymous] }

instance Lean.Lsp.instToJsonRange:

Lean.ToJson Lean.Lsp.Range

Equations

Lean.Lsp.instToJsonRange = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonRange:

Lean.FromJson Lean.Lsp.Range

Equations

Lean.Lsp.instFromJsonRange = { fromJson? := [anonymous] }

instance Lean.Lsp.instOrdRange:

Ord Lean.Lsp.Range

Equations

Lean.Lsp.instOrdRange = { compare := [anonymous] }

instance Lean.Lsp.instLTRange:

LT Lean.Lsp.Range

Equations

Lean.Lsp.instLTRange = ltOfOrd

instance Lean.Lsp.instLERange:

LE Lean.Lsp.Range

Equations

Lean.Lsp.instLERange = leOfOrd

structure Lean.Lsp.Location:

Type

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

instance Lean.Lsp.instInhabitedLocation:

Inhabited Lean.Lsp.Location

Equations

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

instance Lean.Lsp.instBEqLocation:

BEq Lean.Lsp.Location

Equations

Lean.Lsp.instBEqLocation = { beq := [anonymous] }

instance Lean.Lsp.instToJsonLocation:

Lean.ToJson Lean.Lsp.Location

Equations

Lean.Lsp.instToJsonLocation = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonLocation:

Lean.FromJson Lean.Lsp.Location

Equations

Lean.Lsp.instFromJsonLocation = { fromJson? := [anonymous] }

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

Equations

Lean.Lsp.instToJsonLocationLink = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonLocationLink:

Lean.FromJson Lean.Lsp.LocationLink

Equations

Lean.Lsp.instFromJsonLocationLink = { fromJson? := [anonymous] }

structure Lean.Lsp.Command:

Type

title : String
command : String
arguments? : Option (Array Lean.Json)

instance Lean.Lsp.instToJsonCommand:

Lean.ToJson Lean.Lsp.Command

Equations

Lean.Lsp.instToJsonCommand = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonCommand:

Lean.FromJson Lean.Lsp.Command

Equations

Lean.Lsp.instFromJsonCommand = { fromJson? := [anonymous] }

structure Lean.Lsp.TextEdit:

Type

range : Lean.Lsp.Range
newText : String

instance Lean.Lsp.instToJsonTextEdit:

Lean.ToJson Lean.Lsp.TextEdit

Equations

Lean.Lsp.instToJsonTextEdit = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextEdit:

Lean.FromJson Lean.Lsp.TextEdit

Equations

Lean.Lsp.instFromJsonTextEdit = { fromJson? := [anonymous] }

def Lean.Lsp.TextEditBatch:

Type

Equations

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

instance Lean.Lsp.instFromJsonTextEditBatch:

Lean.FromJson Lean.Lsp.TextEditBatch

Equations

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

instance Lean.Lsp.instToJsonTextEditBatch:

Lean.ToJson Lean.Lsp.TextEditBatch

Equations

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

structure Lean.Lsp.TextDocumentIdentifier:

Type

uri : Lean.Lsp.DocumentUri

instance Lean.Lsp.instToJsonTextDocumentIdentifier:

Lean.ToJson Lean.Lsp.TextDocumentIdentifier

Equations

Lean.Lsp.instToJsonTextDocumentIdentifier = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentIdentifier:

Lean.FromJson Lean.Lsp.TextDocumentIdentifier

Equations

Lean.Lsp.instFromJsonTextDocumentIdentifier = { fromJson? := [anonymous] }

structure Lean.Lsp.VersionedTextDocumentIdentifier:

Type

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

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier:

Lean.ToJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

Lean.Lsp.instToJsonVersionedTextDocumentIdentifier = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier:

Lean.FromJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier = { fromJson? := [anonymous] }

structure Lean.Lsp.TextDocumentEdit:

Type

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

instance Lean.Lsp.instToJsonTextDocumentEdit:

Lean.ToJson Lean.Lsp.TextDocumentEdit

Equations

Lean.Lsp.instToJsonTextDocumentEdit = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentEdit:

Lean.FromJson Lean.Lsp.TextDocumentEdit

Equations

Lean.Lsp.instFromJsonTextDocumentEdit = { fromJson? := [anonymous] }

structure Lean.Lsp.TextDocumentItem:

Type

uri : Lean.Lsp.DocumentUri
languageId : String
version : Nat
text : String

instance Lean.Lsp.instToJsonTextDocumentItem:

Lean.ToJson Lean.Lsp.TextDocumentItem

Equations

Lean.Lsp.instToJsonTextDocumentItem = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentItem:

Lean.FromJson Lean.Lsp.TextDocumentItem

Equations

Lean.Lsp.instFromJsonTextDocumentItem = { fromJson? := [anonymous] }

structure Lean.Lsp.TextDocumentPositionParams:

Type

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

instance Lean.Lsp.instToJsonTextDocumentPositionParams:

Lean.ToJson Lean.Lsp.TextDocumentPositionParams

Equations

Lean.Lsp.instToJsonTextDocumentPositionParams = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentPositionParams:

Lean.FromJson Lean.Lsp.TextDocumentPositionParams

Equations

Lean.Lsp.instFromJsonTextDocumentPositionParams = { fromJson? := [anonymous] }

instance Lean.Lsp.instToStringTextDocumentPositionParams:

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

Lean.ToJson Lean.Lsp.DocumentFilter

Equations

Lean.Lsp.instToJsonDocumentFilter = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonDocumentFilter:

Lean.FromJson Lean.Lsp.DocumentFilter

Equations

Lean.Lsp.instFromJsonDocumentFilter = { fromJson? := [anonymous] }

def Lean.Lsp.DocumentSelector:

Type

Equations

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

instance Lean.Lsp.instFromJsonDocumentSelector:

Lean.FromJson Lean.Lsp.DocumentSelector

Equations

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

instance Lean.Lsp.instToJsonDocumentSelector:

Lean.ToJson Lean.Lsp.DocumentSelector

Equations

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

structure Lean.Lsp.StaticRegistrationOptions:

Type

id? : Option String

instance Lean.Lsp.instToJsonStaticRegistrationOptions:

Lean.ToJson Lean.Lsp.StaticRegistrationOptions

Equations

Lean.Lsp.instToJsonStaticRegistrationOptions = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonStaticRegistrationOptions:

Lean.FromJson Lean.Lsp.StaticRegistrationOptions

Equations

Lean.Lsp.instFromJsonStaticRegistrationOptions = { fromJson? := [anonymous] }

structure Lean.Lsp.TextDocumentRegistrationOptions:

Type

documentSelector? : Option Lean.Lsp.DocumentSelector

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions:

Lean.ToJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

Lean.Lsp.instToJsonTextDocumentRegistrationOptions = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions:

Lean.FromJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

Lean.Lsp.instFromJsonTextDocumentRegistrationOptions = { fromJson? := [anonymous] }

inductive Lean.Lsp.MarkupKind:

Type

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

instance Lean.Lsp.instFromJsonMarkupKind:

Lean.FromJson Lean.Lsp.MarkupKind

Equations

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

instance Lean.Lsp.instToJsonMarkupKind:

Lean.ToJson Lean.Lsp.MarkupKind

Equations

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

structure Lean.Lsp.MarkupContent:

Type

kind : Lean.Lsp.MarkupKind
value : String

instance Lean.Lsp.instToJsonMarkupContent:

Lean.ToJson Lean.Lsp.MarkupContent

Equations

Lean.Lsp.instToJsonMarkupContent = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonMarkupContent:

Lean.FromJson Lean.Lsp.MarkupContent

Equations

Lean.Lsp.instFromJsonMarkupContent = { fromJson? := [anonymous] }

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

Type

token : String
value : α

instance Lean.Lsp.instToJsonProgressParams:

{α : Type} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Lsp.ProgressParams α)

Equations

Lean.Lsp.instToJsonProgressParams = { toJson := [anonymous] }

structure Lean.Lsp.WorkDoneProgressReport:

Type

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

instance Lean.Lsp.instToJsonWorkDoneProgressReport:

Lean.ToJson Lean.Lsp.WorkDoneProgressReport

Equations

Lean.Lsp.instToJsonWorkDoneProgressReport = { toJson := [anonymous] }

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

Type

title : String

instance Lean.Lsp.instToJsonWorkDoneProgressBegin:

Lean.ToJson Lean.Lsp.WorkDoneProgressBegin

Equations

Lean.Lsp.instToJsonWorkDoneProgressBegin = { toJson := [anonymous] }

structure Lean.Lsp.WorkDoneProgressEnd:

Type

kind : String
message? : Option String

instance Lean.Lsp.instToJsonWorkDoneProgressEnd:

Lean.ToJson Lean.Lsp.WorkDoneProgressEnd

Equations

Lean.Lsp.instToJsonWorkDoneProgressEnd = { toJson := [anonymous] }