Allows LSP clients to make Remote Procedure Calls to the server.
The single use case for these is to allow the infoview UI to refer to and manipulate heavy-weight
objects residing on the server. It would be inefficient to serialize these into JSON and send over.
For example, the client can format an Expr without transporting the whole Environment.
All RPC requests are relative to an open file and an RPC session for that file. The client must
first connect to the session using $/lean/rpc/connect.
- aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef DynamicObjects that are being kept alive for the RPC client, together with their type names, mapped to by their RPC reference. Note that we may currently have multiple references to the same object. It is only disposed of once all of those are gone. This simplifies the client a bit as it can drop every reference received separately. 
- nextRef : USizeValue to use for the next RpcRef. It is monotonically increasing to avoid any possible bugs resulting from its reuse.
Instances For
Instances For
Instances For
Instances For
- rpcEncode : α → StateM Lean.Server.RpcObjectStore Lean.Json
RpcEncodable α means that α can be serialized in the RPC system of the Lean server.
This is required when α contains fields which should be serialized as an RPC reference
instead of being sent in full.
The type wrapper WithRpcRef is used for these fields which should be sent as
a reference.
- Any type with FromJsonandToJsoninstance is automaticallyRpcEncodable.
- If a type has an Dynamicinstance, thenWithRpcRefcan be used for its references.
- deriving RpcEncodableacts like- FromJson/- ToJsonbut marshalls any- WithRpcReffields as- Lsp.RpcRefs.
Instances
- val : α
Marks fields to encode as opaque references in LSP packets.