Lean.Data.Lsp.InitShutdown

source

structure Lean.Lsp.ClientInfo :

Type

name : String
version? : Option String

source

instance Lean.Lsp.instToJsonClientInfo :

Lean.ToJson Lean.Lsp.ClientInfo

Equations

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

source

instance Lean.Lsp.instFromJsonClientInfo :

Lean.FromJson Lean.Lsp.ClientInfo

Equations

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

source

inductive Lean.Lsp.Trace :

Type

off: Lean.Lsp.Trace
messages: Lean.Lsp.Trace
verbose: Lean.Lsp.Trace

source

instance Lean.Lsp.instFromJsonTrace :

Lean.FromJson Lean.Lsp.Trace

Equations

Lean.Lsp.instFromJsonTrace = { fromJson? := fun j => match Lean.Json.getStr? j with | Except.ok "off" => pure Lean.Lsp.Trace.off | Except.ok "messages" => pure Lean.Lsp.Trace.messages | Except.ok "verbose" => pure Lean.Lsp.Trace.verbose | x => throw "uknown trace" }

source

instance Lean.Lsp.Trace.hasToJson :

Lean.ToJson Lean.Lsp.Trace

Equations

Lean.Lsp.Trace.hasToJson = { toJson := fun x => match x with | Lean.Lsp.Trace.off => Lean.Json.str "off" | Lean.Lsp.Trace.messages => Lean.Json.str "messages" | Lean.Lsp.Trace.verbose => Lean.Json.str "verbose" }

source

structure Lean.Lsp.InitializationOptions :

Type

editDelay? : Option Nat
hasWidgets? : Option Bool

source

instance Lean.Lsp.instFromJsonInitializationOptions :

Lean.FromJson Lean.Lsp.InitializationOptions

Equations

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

source

instance Lean.Lsp.instToJsonInitializationOptions :

Lean.ToJson Lean.Lsp.InitializationOptions

Equations

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

source

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)

source

instance Lean.Lsp.instToJsonInitializeParams :

Lean.ToJson Lean.Lsp.InitializeParams

Equations

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

source

instance Lean.Lsp.instFromJsonInitializeParams :

Lean.FromJson Lean.Lsp.InitializeParams

Equations

Lean.Lsp.instFromJsonInitializeParams = { fromJson? := fun j => let processId? := Lean.Json.getObjValAs? j Int "processId"; let clientInfo? := Lean.Json.getObjValAs? j Lean.Lsp.ClientInfo "clientInfo"; let rootUri? := Lean.Json.getObjValAs? j String "rootUri"; let initializationOptions? := Lean.Json.getObjValAs? j Lean.Lsp.InitializationOptions "initializationOptions"; do let capabilities ← Lean.Json.getObjValAs? j Lean.Lsp.ClientCapabilities "capabilities" let trace : Lean.Lsp.Trace := Option.getD (Except.toOption (Lean.Json.getObjValAs? j Lean.Lsp.Trace "trace")) Lean.Lsp.Trace.off let workspaceFolders? : Except String (Array Lean.Lsp.WorkspaceFolder) := Lean.Json.getObjValAs? j (Array Lean.Lsp.WorkspaceFolder) "workspaceFolders" pure { processId? := Except.toOption processId?, clientInfo? := Except.toOption clientInfo?, rootUri? := Except.toOption rootUri?, initializationOptions? := Except.toOption initializationOptions?, capabilities := capabilities, trace := trace, workspaceFolders? := Except.toOption workspaceFolders? } }

source

inductive Lean.Lsp.InitializedParams :

Type

mk: Lean.Lsp.InitializedParams

source

instance Lean.Lsp.instFromJsonInitializedParams :

Lean.FromJson Lean.Lsp.InitializedParams

Equations

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

source

instance Lean.Lsp.instToJsonInitializedParams :

Lean.ToJson Lean.Lsp.InitializedParams

Equations

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

source

structure Lean.Lsp.ServerInfo :

Type

name : String
version? : Option String

source

instance Lean.Lsp.instFromJsonServerInfo :

Lean.FromJson Lean.Lsp.ServerInfo

Equations

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

source

instance Lean.Lsp.instToJsonServerInfo :

Lean.ToJson Lean.Lsp.ServerInfo

Equations

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

source

structure Lean.Lsp.InitializeResult :

Type

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

source

instance Lean.Lsp.instToJsonInitializeResult :

Lean.ToJson Lean.Lsp.InitializeResult

Equations

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

source

instance Lean.Lsp.instFromJsonInitializeResult :

Lean.FromJson Lean.Lsp.InitializeResult

Equations

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