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

Equations

• Lean.Lsp.instToJsonClientInfo = { toJson := Lean.Lsp.instToJsonClientInfo.toJson }

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

Equations

• Lean.Lsp.instToJsonClientInfo.toJson x✝ = Lean.Json.mkObj [[("name", Lean.toJson x✝.name)], Lean.Json.opt "version" x✝.version?].flatten

instance Lean.Lsp.instFromJsonClientInfo : FromJson ClientInfo

Equations

• Lean.Lsp.instFromJsonClientInfo = { fromJson? := Lean.Lsp.instFromJsonClientInfo.fromJson }

def Lean.Lsp.instFromJsonClientInfo.fromJson : Json → Except String ClientInfo

Equations

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

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

Equations

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

instance Lean.Lsp.Trace.hasToJson : ToJson Trace

Equations

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

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

Equations

• Lean.Lsp.instToJsonHashSet = { toJson := fun (s : Std.HashSet α) => Lean.Json.arr (Array.map Lean.toJson s.toArray) }

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

Equations

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

structure Lean.Lsp.LogConfig : Type

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

instance Lean.Lsp.instFromJsonLogConfig : FromJson LogConfig

Equations

• Lean.Lsp.instFromJsonLogConfig = { fromJson? := Lean.Lsp.instFromJsonLogConfig.fromJson }

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

Equations

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

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

Equations

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

instance Lean.Lsp.instToJsonLogConfig : ToJson LogConfig

Equations

• Lean.Lsp.instToJsonLogConfig = { toJson := Lean.Lsp.instToJsonLogConfig.toJson }

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

Equations

• Lean.Lsp.instToJsonInitializationOptions.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "hasWidgets" x✝.hasWidgets?, Lean.Json.opt "logCfg" x✝.logCfg?].flatten

instance Lean.Lsp.instToJsonInitializationOptions : ToJson InitializationOptions

Equations

• Lean.Lsp.instToJsonInitializationOptions = { toJson := Lean.Lsp.instToJsonInitializationOptions.toJson }

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

Equations

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

instance Lean.Lsp.instFromJsonInitializationOptions : FromJson InitializationOptions

Equations

• Lean.Lsp.instFromJsonInitializationOptions = { fromJson? := Lean.Lsp.instFromJsonInitializationOptions.fromJson }

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

Equations

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

instance Lean.Lsp.instToJsonInitializeParams : ToJson InitializeParams

Equations

• Lean.Lsp.instToJsonInitializeParams = { toJson := Lean.Lsp.instToJsonInitializeParams.toJson }

instance Lean.Lsp.instFromJsonInitializeParams : FromJson InitializeParams

Equations

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

inductive Lean.Lsp.InitializedParams : Type

• mk : InitializedParams

instance Lean.Lsp.instFromJsonInitializedParams : FromJson InitializedParams

Equations

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

instance Lean.Lsp.instToJsonInitializedParams : ToJson InitializedParams

Equations

• Lean.Lsp.instToJsonInitializedParams = { toJson := fun (x : Lean.Lsp.InitializedParams) => Lean.Json.null }

structure Lean.Lsp.ServerInfo : Type

• name : String
• version? : Option String

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

Equations

• Lean.Lsp.instToJsonServerInfo.toJson x✝ = Lean.Json.mkObj [[("name", Lean.toJson x✝.name)], Lean.Json.opt "version" x✝.version?].flatten

instance Lean.Lsp.instToJsonServerInfo : ToJson ServerInfo

Equations

• Lean.Lsp.instToJsonServerInfo = { toJson := Lean.Lsp.instToJsonServerInfo.toJson }

instance Lean.Lsp.instFromJsonServerInfo : FromJson ServerInfo

Equations

• Lean.Lsp.instFromJsonServerInfo = { fromJson? := Lean.Lsp.instFromJsonServerInfo.fromJson }

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

Equations

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

structure Lean.Lsp.InitializeResult : Type

• capabilities : ServerCapabilities
• serverInfo? : Option ServerInfo

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

Equations

• Lean.Lsp.instToJsonInitializeResult.toJson x✝ = Lean.Json.mkObj [[("capabilities", Lean.toJson x✝.capabilities)], Lean.Json.opt "serverInfo" x✝.serverInfo?].flatten

instance Lean.Lsp.instToJsonInitializeResult : ToJson InitializeResult

Equations

• Lean.Lsp.instToJsonInitializeResult = { toJson := Lean.Lsp.instToJsonInitializeResult.toJson }

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

Equations

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

instance Lean.Lsp.instFromJsonInitializeResult : FromJson InitializeResult

Equations

• Lean.Lsp.instFromJsonInitializeResult = { fromJson? := Lean.Lsp.instFromJsonInitializeResult.fromJson }