Functionality to do with initializing and shutting down the server ("General Messages" section of LSP spec).
- off: Lean.Lsp.Trace
- messages: Lean.Lsp.Trace
- verbose: Lean.Lsp.Trace
A TraceValue represents the level of verbosity with which the server systematically reports its execution trace using $/logTrace
notifications.
reference
Instances For
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.
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.
Lean-specific initialization options.
Instances For
- clientInfo? : Option Lean.Lsp.ClientInfo
- initializationOptions? : Option Lean.Lsp.InitializationOptions
- capabilities : Lean.Lsp.ClientCapabilities
- trace : Lean.Lsp.Trace
If omitted, we default to off.
- workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)
Instances For
Instances For
- capabilities : Lean.Lsp.ServerCapabilities
- serverInfo? : Option Lean.Lsp.ServerInfo