Interface RpcSessionAtPos

An RpcSessionForFile with call specialized to a specific position p.

Morally, this bundles an RPC session with the set of RPC methods available at the position p.

It is okay to mix RPC references between different RpcSessionAtPos objects created from the same RpcSessionForFile.

interface RpcSessionAtPos {
    call<T, S>(
        method: string,
        params: T,
        options?: ClientRequestOptions,
    ): Promise<S>;
}

Index

Methods

Methods

call

call<T, S>(
    method: string,
    params: T,
    options?: ClientRequestOptions,
): Promise<S>
Invoke an RPC method in the Lean server.
Type Parameters
- T
- S
Parameters
- method: string
  fully qualified name of the method to call.
- params: T
  arguments to the invoked method.
- Optionaloptions: ClientRequestOptions
  additional configuration for the request.
Returns Promise<S>
a promise that resolves to the returned value, or an error in case the call fails.
- Defined in lean4-infoview-api/dist/rpcSessions.d.ts:50