Documentation

Lean.Data.Lsp.InitShutdown

Functionality to do with initializing and shutting down the server ("General Messages" section of LSP spec).

structure Lean.Lsp.ClientInfo:

Type

name : String
version? : Option String

instance Lean.Lsp.instToJsonClientInfo:

Lean.ToJson Lean.Lsp.ClientInfo

Equations

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

instance Lean.Lsp.instFromJsonClientInfo:

Lean.FromJson Lean.Lsp.ClientInfo

Equations

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

inductive Lean.Lsp.Trace:

Type

instance Lean.Lsp.instFromJsonTrace:

Lean.FromJson Lean.Lsp.Trace

Equations

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

instance Lean.Lsp.Trace.hasToJson:

Lean.ToJson Lean.Lsp.Trace

Equations

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

structure Lean.Lsp.InitializationOptions:

Type

Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editors feel faster at the cost of higher CPU usage. Defaults to 200ms.
editDelay? : Option Nat
Whether the client supports interactive widgets. When true, in order to improve performance the server may cease including information which can be retrieved interactively in some standard LSP messages. Defaults to false.
hasWidgets? : Option Bool

Lean-specific initialization options.

instance Lean.Lsp.instToJsonInitializationOptions:

Lean.ToJson Lean.Lsp.InitializationOptions

Equations

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

instance Lean.Lsp.instFromJsonInitializationOptions:

Lean.FromJson Lean.Lsp.InitializationOptions

Equations

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

structure Lean.Lsp.InitializeParams:

Type

processId? : Option Int
clientInfo? : Option Lean.Lsp.ClientInfo
rootUri? : Option String
initializationOptions? : Option Lean.Lsp.InitializationOptions
capabilities : Lean.Lsp.ClientCapabilities
trace : Lean.Lsp.Trace
workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)

instance Lean.Lsp.instToJsonInitializeParams:

Lean.ToJson Lean.Lsp.InitializeParams

Equations

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

instance Lean.Lsp.instFromJsonInitializeParams:

Lean.FromJson Lean.Lsp.InitializeParams

Equations

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

inductive Lean.Lsp.InitializedParams:

Type

mk: Lean.Lsp.InitializedParams

instance Lean.Lsp.instFromJsonInitializedParams:

Lean.FromJson Lean.Lsp.InitializedParams

Equations

Lean.Lsp.instFromJsonInitializedParams = { fromJson? := fun x => pure Lean.Lsp.InitializedParams.mk }

instance Lean.Lsp.instToJsonInitializedParams:

Lean.ToJson Lean.Lsp.InitializedParams

Equations

Lean.Lsp.instToJsonInitializedParams = { toJson := fun x => Lean.Json.null }

structure Lean.Lsp.ServerInfo:

Type

name : String
version? : Option String

instance Lean.Lsp.instToJsonServerInfo:

Lean.ToJson Lean.Lsp.ServerInfo

Equations

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

instance Lean.Lsp.instFromJsonServerInfo:

Lean.FromJson Lean.Lsp.ServerInfo

Equations

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

structure Lean.Lsp.InitializeResult:

Type

capabilities : Lean.Lsp.ServerCapabilities
serverInfo? : Option Lean.Lsp.ServerInfo

instance Lean.Lsp.instToJsonInitializeResult:

Lean.ToJson Lean.Lsp.InitializeResult

Equations

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

instance Lean.Lsp.instFromJsonInitializeResult:

Lean.FromJson Lean.Lsp.InitializeResult

Equations

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