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

@[implicit_reducible]

instance Lean.Lsp.instToJsonClientInfo : ToJson ClientInfo

def Lean.Lsp.instToJsonClientInfo.toJson : ClientInfo → Json

@[implicit_reducible]

instance Lean.Lsp.instFromJsonClientInfo : FromJson ClientInfo

def Lean.Lsp.instFromJsonClientInfo.fromJson : Json → Except String 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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonTrace : FromJson Trace

@[implicit_reducible]

instance Lean.Lsp.Trace.hasToJson : ToJson Trace

@[implicit_reducible]

def Lean.Lsp.instToJsonHashSet {α : Type u_1} [BEq α] [Hashable α] [ToJson α] : ToJson (Std.HashSet α)

@[implicit_reducible]

def Lean.Lsp.instFromJsonHashSet {α : Type u_1} [BEq α] [Hashable α] [FromJson α] : FromJson (Std.HashSet α)

structure Lean.Lsp.LogConfig : Type

• logDir? : Option System.FilePath
• allowedMethods? : Option (Std.HashSet String)
• disallowedMethods? : Option (Std.HashSet String)

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLogConfig : FromJson LogConfig

def Lean.Lsp.instFromJsonLogConfig.fromJson : Json → Except String LogConfig

def Lean.Lsp.instToJsonLogConfig.toJson : LogConfig → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonLogConfig : ToJson LogConfig

structure Lean.Lsp.InitializationOptions : Type

Lean-specific initialization options.

• 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.

• logCfg? : Option LogConfig

def Lean.Lsp.instToJsonInitializationOptions.toJson : InitializationOptions → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonInitializationOptions : ToJson InitializationOptions

def Lean.Lsp.instFromJsonInitializationOptions.fromJson : Json → Except String InitializationOptions

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInitializationOptions : FromJson InitializationOptions

structure Lean.Lsp.InitializeParams : Type

• processId? : Option Int
• clientInfo? : Option ClientInfo
• rootUri? : Option String

  Not used by the language server. We use the cwd of the server process instead.

• initializationOptions? : Option InitializationOptions
• capabilities : ClientCapabilities
• trace : Trace

  If omitted, we default to off.

• workspaceFolders? : Option (Array WorkspaceFolder)

def Lean.Lsp.instToJsonInitializeParams.toJson : InitializeParams → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonInitializeParams : ToJson InitializeParams

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInitializeParams : FromJson InitializeParams

inductive Lean.Lsp.InitializedParams : Type

• mk : InitializedParams

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInitializedParams : FromJson InitializedParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonInitializedParams : ToJson InitializedParams

structure Lean.Lsp.ServerInfo : Type

• name : String
• version? : Option String

def Lean.Lsp.instToJsonServerInfo.toJson : ServerInfo → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonServerInfo : ToJson ServerInfo

@[implicit_reducible]

instance Lean.Lsp.instFromJsonServerInfo : FromJson ServerInfo

def Lean.Lsp.instFromJsonServerInfo.fromJson : Json → Except String ServerInfo

structure Lean.Lsp.InitializeResult : Type

• capabilities : ServerCapabilities
• serverInfo? : Option ServerInfo

def Lean.Lsp.instToJsonInitializeResult.toJson : InitializeResult → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonInitializeResult : ToJson InitializeResult

def Lean.Lsp.instFromJsonInitializeResult.fromJson : Json → Except String InitializeResult

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInitializeResult : FromJson InitializeResult