OptionalfailedIf present, stores a fatal exception indicating that the RPC session can no longer be used. For example: the worker crashed
Returns this session with call specialized to position within the file.
This is guaranteed to return the same (by reference) object
if called multiple times with the same (by deep comparison) position,
on the same RpcSessionForFile.
It can therefore be used as a React dep.
Invoke an RPC method in the Lean server.
To compute the set of RPC methods that can be called,
the server finds the environment e at the source code location this.uri:position.
The callable methods are then all the builtin ones,
and all constants in e marked with @[server_rpc_method]
(i.e., the @[server_rpc_method] declarations made above this.uri:position).
within the file identified by uri, used to resolve the set of available RPC methods.
fully qualified name of the method to call.
arguments to the invoked method.
Optionaloptions: ClientRequestOptions
additional configuration for the request.
a promise that resolves to the returned value, or to an error in case the call fails.
Traverses an object received from the RPC server and registers all contained references for future garbage collection.
The function implements a form of "conservative garbage collection"
where it treats any subobject {'__rpcref': v} as a potential RPC reference.
Therefore __rpcref should not be used as a field name on the Lean side
to prevent false positives.
Earlier versions of the extension had manually written registration functions for every type, but those are a lot of boilerplate. If we change back to that approach, we should generate them automatically. It would also be possible to move to a new RPC wire format that specifies which values are references using metadata.
Manages a connection to an RPC session that has been opened for a given file (in the Lean server's worker process for that file).
An RPC session keeps track of a set of RPC references that are mutually intelligible, in the sense that any RPC method can be called with any number of references from this set. On the other hand, it is not possible to mix RPC references between different sessions.