Lean.Data.Lsp.Capabilities

Minimal LSP servers/clients do not have to implement a lot of functionality. Most useful additional behavior is instead opted into via capabilities.

source

structure Lean.Lsp.CompletionItemCapabilities:

Type

insertReplaceSupport? : Option Bool

source

instance Lean.Lsp.instToJsonCompletionItemCapabilities:

Lean.ToJson Lean.Lsp.CompletionItemCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonCompletionItemCapabilities:

Lean.FromJson Lean.Lsp.CompletionItemCapabilities

Equations

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

source

structure Lean.Lsp.CompletionClientCapabilities:

Type

completionItem? : Option Lean.Lsp.CompletionItemCapabilities

source

instance Lean.Lsp.instToJsonCompletionClientCapabilities:

Lean.ToJson Lean.Lsp.CompletionClientCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonCompletionClientCapabilities:

Lean.FromJson Lean.Lsp.CompletionClientCapabilities

Equations

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

source

structure Lean.Lsp.TextDocumentClientCapabilities:

Type

completion? : Option Lean.Lsp.CompletionClientCapabilities

source

instance Lean.Lsp.instToJsonTextDocumentClientCapabilities:

Lean.ToJson Lean.Lsp.TextDocumentClientCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonTextDocumentClientCapabilities:

Lean.FromJson Lean.Lsp.TextDocumentClientCapabilities

Equations

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

source

structure Lean.Lsp.ShowDocumentClientCapabilities:

Type

support : Bool

source

instance Lean.Lsp.instToJsonShowDocumentClientCapabilities:

Lean.ToJson Lean.Lsp.ShowDocumentClientCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonShowDocumentClientCapabilities:

Lean.FromJson Lean.Lsp.ShowDocumentClientCapabilities

Equations

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

source

structure Lean.Lsp.WindowClientCapabilities:

Type

showDocument? : Option Lean.Lsp.ShowDocumentClientCapabilities

source

instance Lean.Lsp.instToJsonWindowClientCapabilities:

Lean.ToJson Lean.Lsp.WindowClientCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonWindowClientCapabilities:

Lean.FromJson Lean.Lsp.WindowClientCapabilities

Equations

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

source

structure Lean.Lsp.ClientCapabilities:

Type

textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities
window? : Option Lean.Lsp.WindowClientCapabilities

source

instance Lean.Lsp.instToJsonClientCapabilities:

Lean.ToJson Lean.Lsp.ClientCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonClientCapabilities:

Lean.FromJson Lean.Lsp.ClientCapabilities

Equations

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

source

structure Lean.Lsp.ServerCapabilities:

Type

textDocumentSync? : Option Lean.Lsp.TextDocumentSyncOptions
completionProvider? : Option Lean.Lsp.CompletionOptions
hoverProvider : Bool
documentHighlightProvider : Bool
documentSymbolProvider : Bool
definitionProvider : Bool
declarationProvider : Bool
typeDefinitionProvider : Bool
referencesProvider : Bool
workspaceSymbolProvider : Bool
foldingRangeProvider : Bool
semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions

source

instance Lean.Lsp.instToJsonServerCapabilities:

Lean.ToJson Lean.Lsp.ServerCapabilities

Equations

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

source

instance Lean.Lsp.instFromJsonServerCapabilities:

Lean.FromJson Lean.Lsp.ServerCapabilities

Equations

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