This file contains Lean-specific extensions to LSP. See the structures below for which additional requests and notifications are supported.
- version : Nat
textDocument/waitForDiagnostics client->server request.
Yields a response when all the diagnostics for a version of the document greater or equal to the specified one have been emitted. If the request specifies a version above the most recently processed one, the server will delay the response until it does receive the specified version. Exists for synchronization purposes, e.g. during testing or when external tools might want to use our LSP server.
- textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
$/lean/fileProgress client<-server notification.
Contains the ranges of the document that are currently being processed by the server.
$/lean/rpc/connect client->server request.
Starts an RPC session at the given file's worker, replying with the new session ID. Multiple sessions may be started and operating concurrently.
A session may be destroyed by the server at any time (e.g. due to a crash), in which case further
RPC requests for that session will reply with
RpcNeedsReconnect errors. The client should discard
references held from that session and
- textDocument : Lean.Lsp.TextDocumentIdentifier
- position : Lean.Lsp.Position
- method : Lake.Name
Procedure to invoke. Must be fully qualified.
- params : Lean.Json
$/lean/rpc/call client->server request.
A request to execute a procedure bound for RPC. If an incorrect session ID is present, the server
Extending TDPP is weird. But in Lean, symbols exist in the context of a position within a source file. So we need this to refer to code in the environment at that position.
$/lean/rpc/release client->server notification.
A notification to release remote references. Should be sent by the client when it no longer needs
RpcRefs it has previously received from the server. Not doing so is safe but will leak memory.
$/lean/rpc/keepAlive client->server notification.
The client must send an RPC notification every 10s in order to keep the RPC session alive. This is the simplest one. On not seeing any notifications for three 10s periods, the server will drop the RPC session and its associated references.