@leanprover/infoview
    Preparing search index...

    Interface EditorApi

    Interface that the InfoView WebView uses to talk to the hosting editor.

    interface EditorApi {
        applyEdit(te: WorkspaceEdit): Promise<void>;
        closeRpcSession(sessionId: string): Promise<void>;
        copyToClipboard(text: string): Promise<void>;
        createRpcSession(uri: string): Promise<string>;
        insertText(
            text: string,
            kind: TextInsertKind,
            pos?: TextDocumentPositionParams,
        ): Promise<void>;
        restartFile(uri: string): Promise<void>;
        saveConfig(config: InfoviewConfig): Promise<any>;
        sendClientNotification(
            uri: string,
            method: string,
            params: any,
        ): Promise<void>;
        sendClientRequest(
            uri: string,
            method: string,
            params: any,
            options?: ClientRequestOptions,
        ): Promise<any>;
        showDocument(show: ShowDocumentParams): Promise<void>;
        subscribeClientNotifications(method: string): Promise<void>;
        subscribeServerNotifications(method: string): Promise<void>;
        unsubscribeClientNotifications(method: string): Promise<void>;
        unsubscribeServerNotifications(method: string): Promise<void>;
    }
    Index
    • Applies the given WorkspaceEdit to the workspace.

      Parameters

      Returns Promise<void>

    • Closes an RPC session created with createRpcSession.

      Parameters

      • sessionId: string

      Returns Promise<void>

    • Put text in the user's clipboard.

      Parameters

      • text: string

      Returns Promise<void>

    • Creates an RPC session for the given uri and returns the session id. The extension takes care of keeping the RPC session alive. (The infoview cannot reliably send keep-alive messages because setInterval is throttled in the infoview when the vscode window is not visible.)

      Parameters

      • uri: string

      Returns Promise<string>

    • Restarts the given file.

      Parameters

      • uri: string

      Returns Promise<void>

    • Send a notification to the LSP server.

      Parameters

      • uri: string
      • method: string
      • params: any

      Returns Promise<void>

    • Make a request to the LSP server.

      Parameters

      Returns Promise<any>

    • Like subscribeServerNotifications, but for client->server notifications.

      Parameters

      • method: string

      Returns Promise<void>

    • Subscribe to notifications from the LSP server with the specified method. Notifications which have been subscribed to will be fired through InfoviewApi.gotServerNotification. This may be called multiple times, in which case the editor must count the subscriptions and only stop firing events when unsubscribe has been called the same amount of times.

      Parameters

      • method: string

      Returns Promise<void>

    • Parameters

      • method: string

      Returns Promise<void>

    • Parameters

      • method: string

      Returns Promise<void>