@leanprover/infoview
    Preparing search index...

    Interface RpcServerIface

    Abstraction of the functionality needed to establish RPC sessions in the Lean server and to make RPC calls. See the Lean module Lean.Server.Rpc.Basic.

    This interface can be implemented both in the infoview (relaying LSP messages from the webview to the extension), as well as in the extension itself (directly sending LSP messages via the vscode-languageserver-node library (TODO)).

    interface RpcServerIface {
        call(
            request: RpcCallParams,
            options?: ClientRequestOptions,
        ): Promise<any>;
        closeRpcSession(sessionId: string): void;
        createRpcSession(uri: string): Promise<string>;
        release(request: RpcReleaseParams): void;
    }
    Index
    call closeRpcSession createRpcSession release

    • Closes an RPC session created with createRpcSession.

      Parameters

      • sessionId: string

      Returns void

    • Creates an RPC session for the given URI and returns the session ID. The implementation of RpcServerIface takes care to send any required keepalive notifications.

      Parameters

      • uri: string

      Returns Promise<string>

    • Sends an RPC reference release notification to the server.

      Parameters

      Returns void

    Settings
    Member Visibility

    On This Page
    Methods