Lean.Data.Lsp.Basic

source

structure Lean.Lsp.CancelParams :

Type

id : Lean.JsonRpc.RequestID

source

instance Lean.Lsp.instInhabitedCancelParams :

Inhabited Lean.Lsp.CancelParams

Equations

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

source

instance Lean.Lsp.instToJsonCancelParams :

Lean.ToJson Lean.Lsp.CancelParams

Equations

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

source

instance Lean.Lsp.instFromJsonCancelParams :

Lean.FromJson Lean.Lsp.CancelParams

Equations

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

source

instance Lean.Lsp.instBEqCancelParams :

BEq Lean.Lsp.CancelParams

Equations

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

source

@[inline]

abbrev Lean.Lsp.DocumentUri :

Type

Equations

Lean.Lsp.DocumentUri = String

source

structure Lean.Lsp.Position :

Type

line : Nat
character : Nat

source

instance Lean.Lsp.instToJsonPosition :

Lean.ToJson Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instInhabitedPosition :

Inhabited Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instOrdPosition :

Ord Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instFromJsonPosition :

Lean.FromJson Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instBEqPosition :

BEq Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instHashablePosition :

Hashable Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instToStringPosition :

ToString Lean.Lsp.Position

Equations

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

source

instance Lean.Lsp.instLTPosition :

LT Lean.Lsp.Position

Equations

Lean.Lsp.instLTPosition = ltOfOrd

source

instance Lean.Lsp.instLEPosition :

LE Lean.Lsp.Position

Equations

Lean.Lsp.instLEPosition = leOfOrd

source

structure Lean.Lsp.Range :

Type

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

source

instance Lean.Lsp.instBEqRange :

BEq Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instToJsonRange :

Lean.ToJson Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instHashableRange :

Hashable Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instInhabitedRange :

Inhabited Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instOrdRange :

Ord Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instFromJsonRange :

Lean.FromJson Lean.Lsp.Range

Equations

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

source

instance Lean.Lsp.instLTRange :

LT Lean.Lsp.Range

Equations

Lean.Lsp.instLTRange = ltOfOrd

source

instance Lean.Lsp.instLERange :

LE Lean.Lsp.Range

Equations

Lean.Lsp.instLERange = leOfOrd

source

structure Lean.Lsp.Location :

Type

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

source

instance Lean.Lsp.instBEqLocation :

BEq Lean.Lsp.Location

Equations

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

source

instance Lean.Lsp.instInhabitedLocation :

Inhabited Lean.Lsp.Location

Equations

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

source

instance Lean.Lsp.instToJsonLocation :

Lean.ToJson Lean.Lsp.Location

Equations

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

source

instance Lean.Lsp.instFromJsonLocation :

Lean.FromJson Lean.Lsp.Location

Equations

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

source

structure Lean.Lsp.LocationLink :

Type

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

source

instance Lean.Lsp.instFromJsonLocationLink :

Lean.FromJson Lean.Lsp.LocationLink

Equations

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

source

instance Lean.Lsp.instToJsonLocationLink :

Lean.ToJson Lean.Lsp.LocationLink

Equations

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

source

structure Lean.Lsp.Command :

Type

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

source

instance Lean.Lsp.instToJsonCommand :

Lean.ToJson Lean.Lsp.Command

Equations

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

source

instance Lean.Lsp.instFromJsonCommand :

Lean.FromJson Lean.Lsp.Command

Equations

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

source

structure Lean.Lsp.TextEdit :

Type

range : Lean.Lsp.Range
newText : String

source

instance Lean.Lsp.instToJsonTextEdit :

Lean.ToJson Lean.Lsp.TextEdit

Equations

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

source

instance Lean.Lsp.instFromJsonTextEdit :

Lean.FromJson Lean.Lsp.TextEdit

Equations

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

source

noncomputable def Lean.Lsp.TextEditBatch :

Type

Equations

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

source

instance Lean.Lsp.instFromJsonTextEditBatch :

Lean.FromJson Lean.Lsp.TextEditBatch

Equations

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

source

instance Lean.Lsp.instToJsonTextEditBatch :

Lean.ToJson Lean.Lsp.TextEditBatch

Equations

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

source

structure Lean.Lsp.TextDocumentIdentifier :

Type

uri : Lean.Lsp.DocumentUri

source

instance Lean.Lsp.instToJsonTextDocumentIdentifier :

Lean.ToJson Lean.Lsp.TextDocumentIdentifier

Equations

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

source

instance Lean.Lsp.instFromJsonTextDocumentIdentifier :

Lean.FromJson Lean.Lsp.TextDocumentIdentifier

Equations

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

source

structure Lean.Lsp.VersionedTextDocumentIdentifier :

Type

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

source

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier :

Lean.FromJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

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

source

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier :

Lean.ToJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

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

source

structure Lean.Lsp.TextDocumentEdit :

Type

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

source

instance Lean.Lsp.instFromJsonTextDocumentEdit :

Lean.FromJson Lean.Lsp.TextDocumentEdit

Equations

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

source

instance Lean.Lsp.instToJsonTextDocumentEdit :

Lean.ToJson Lean.Lsp.TextDocumentEdit

Equations

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

source

structure Lean.Lsp.TextDocumentItem :

Type

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

source

instance Lean.Lsp.instFromJsonTextDocumentItem :

Lean.FromJson Lean.Lsp.TextDocumentItem

Equations

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

source

instance Lean.Lsp.instToJsonTextDocumentItem :

Lean.ToJson Lean.Lsp.TextDocumentItem

Equations

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

source

structure Lean.Lsp.TextDocumentPositionParams :

Type

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

source

instance Lean.Lsp.instToJsonTextDocumentPositionParams :

Lean.ToJson Lean.Lsp.TextDocumentPositionParams

Equations

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

source

instance Lean.Lsp.instFromJsonTextDocumentPositionParams :

Lean.FromJson Lean.Lsp.TextDocumentPositionParams

Equations

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

source

structure Lean.Lsp.DocumentFilter :

Type

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

source

instance Lean.Lsp.instFromJsonDocumentFilter :

Lean.FromJson Lean.Lsp.DocumentFilter

Equations

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

source

instance Lean.Lsp.instToJsonDocumentFilter :

Lean.ToJson Lean.Lsp.DocumentFilter

Equations

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

source

noncomputable def Lean.Lsp.DocumentSelector :

Type

Equations

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

source

instance Lean.Lsp.instFromJsonDocumentSelector :

Lean.FromJson Lean.Lsp.DocumentSelector

Equations

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

source

instance Lean.Lsp.instToJsonDocumentSelector :

Lean.ToJson Lean.Lsp.DocumentSelector

Equations

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

source

structure Lean.Lsp.StaticRegistrationOptions :

Type

id? : Option String

source

instance Lean.Lsp.instToJsonStaticRegistrationOptions :

Lean.ToJson Lean.Lsp.StaticRegistrationOptions

Equations

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

source

instance Lean.Lsp.instFromJsonStaticRegistrationOptions :

Lean.FromJson Lean.Lsp.StaticRegistrationOptions

Equations

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

source

structure Lean.Lsp.TextDocumentRegistrationOptions :

Type

documentSelector? : Option Lean.Lsp.DocumentSelector

source

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions :

Lean.ToJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

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

source

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions :

Lean.FromJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

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

source

inductive Lean.Lsp.MarkupKind :

Type

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

source

instance Lean.Lsp.instFromJsonMarkupKind :

Lean.FromJson Lean.Lsp.MarkupKind

Equations

Lean.Lsp.instFromJsonMarkupKind = { fromJson? := fun x => match x with | Lean.Json.str "plaintext" => Except.ok Lean.Lsp.MarkupKind.plaintext | Lean.Json.str "markdown" => Except.ok Lean.Lsp.MarkupKind.markdown | x => throw "unknown MarkupKind" }

source

instance Lean.Lsp.instToJsonMarkupKind :

Lean.ToJson Lean.Lsp.MarkupKind

Equations

Lean.Lsp.instToJsonMarkupKind = { toJson := fun x => match x with | Lean.Lsp.MarkupKind.plaintext => Lean.Json.str "plaintext" | Lean.Lsp.MarkupKind.markdown => Lean.Json.str "markdown" }

source

structure Lean.Lsp.MarkupContent :

Type

kind : Lean.Lsp.MarkupKind
value : String

source

instance Lean.Lsp.instToJsonMarkupContent :

Lean.ToJson Lean.Lsp.MarkupContent

Equations

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

source

instance Lean.Lsp.instFromJsonMarkupContent :

Lean.FromJson Lean.Lsp.MarkupContent

Equations

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

source

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

Type

token : String
value : α

source

instance Lean.Lsp.instToJsonProgressParams :

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

Equations

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

source

structure Lean.Lsp.WorkDoneProgressReport :

Type

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

source

instance Lean.Lsp.instToJsonWorkDoneProgressReport :

Lean.ToJson Lean.Lsp.WorkDoneProgressReport

Equations

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

source

structure Lean.Lsp.WorkDoneProgressBegin extends Lean.Lsp.WorkDoneProgressReport :

Type

title : String

source

instance Lean.Lsp.instToJsonWorkDoneProgressBegin :

Lean.ToJson Lean.Lsp.WorkDoneProgressBegin

Equations

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

source

structure Lean.Lsp.WorkDoneProgressEnd :

Type

kind : String
message? : Option String

source

instance Lean.Lsp.instToJsonWorkDoneProgressEnd :

Lean.ToJson Lean.Lsp.WorkDoneProgressEnd

Equations

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