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 : ToJson ClientInfo

instance Lean.Lsp.instFromJsonClientInfo : FromJson ClientInfo

inductive Lean.Lsp.Trace : Type

A TraceValue represents the level of verbosity with which the server systematically reports its execution trace using $/logTrace notifications. reference

• off : Trace
• messages : Trace
• verbose : Trace

instance Lean.Lsp.instFromJsonTrace : FromJson Trace

instance Lean.Lsp.Trace.hasToJson : ToJson Trace

structure Lean.Lsp.InitializationOptions : Type

Lean-specific initialization options.

• editDelay? : Option Nat

  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.

• hasWidgets? : Option Bool

  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.

instance Lean.Lsp.instToJsonInitializationOptions : ToJson InitializationOptions

instance Lean.Lsp.instFromJsonInitializationOptions : FromJson InitializationOptions

structure Lean.Lsp.InitializeParams : Type

• processId? : Option Int
• clientInfo? : Option ClientInfo
• rootUri? : Option String
• initializationOptions? : Option InitializationOptions
• capabilities : ClientCapabilities
• trace : Trace

  If omitted, we default to off.

• workspaceFolders? : Option (Array WorkspaceFolder)

instance Lean.Lsp.instToJsonInitializeParams : ToJson InitializeParams

def Lean.Lsp.InitializeParams.editDelay (params : InitializeParams) : Nat

instance Lean.Lsp.instFromJsonInitializeParams : FromJson InitializeParams

inductive Lean.Lsp.InitializedParams : Type

• mk : InitializedParams

instance Lean.Lsp.instFromJsonInitializedParams : FromJson InitializedParams

instance Lean.Lsp.instToJsonInitializedParams : ToJson InitializedParams

structure Lean.Lsp.ServerInfo : Type

• name : String
• version? : Option String

instance Lean.Lsp.instToJsonServerInfo : ToJson ServerInfo

instance Lean.Lsp.instFromJsonServerInfo : FromJson ServerInfo

structure Lean.Lsp.InitializeResult : Type

• capabilities : ServerCapabilities
• serverInfo? : Option ServerInfo

instance Lean.Lsp.instToJsonInitializeResult : ToJson InitializeResult

instance Lean.Lsp.instFromJsonInitializeResult : FromJson InitializeResult