@leanprover/infoview
    Preparing search index...

    Interface InfoviewApi

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

    interface InfoviewApi {
        changedCursorLocation(loc?: Location): Promise<void>;
        changedInfoviewConfig(conf: InfoviewConfig): Promise<void>;
        clickedContextMenu(action: ContextMenuAction): Promise<void>;
        getInfoviewHtml(): Promise<string>;
        gotServerNotification(method: string, params: any): Promise<void>;
        initialize(loc: Location): Promise<void>;
        requestedAction(action: InfoviewAction): Promise<void>;
        runTestScript(javaScript: string): Promise<void>;
        sentClientNotification(method: string, params: any): Promise<void>;
        serverRestarted(
            serverInitializeResult: InitializeResult<LeanServerCapabilities>,
        ): Promise<void>;
        serverStopped(
            serverStoppedReason: ServerStoppedReason | undefined,
        ): Promise<void>;
    }
    Index
    changedCursorLocation changedInfoviewConfig clickedContextMenu getInfoviewHtml gotServerNotification initialize requestedAction runTestScript sentClientNotification serverRestarted serverStopped

    • Must fire whenever the user moves their cursor or makes a selection while in a Lean file. Movements in other kinds of files must not fire this event. When no selection is made, loc.range.start must equal loc.range.end.

      Parameters

      Returns Promise<void>

    • Must fire whenever the infoview configuration changes.

      Parameters

      Returns Promise<void>

    • Must fire whenever the user clicks an infoview-specific context menu entry.

      Parameters

      Returns Promise<void>

    • Return the current HTML contents of the infoview as a string. This is used for testing, in particular to inspect the page contents and check if the UI is in a correct state.

      Returns Promise<string>

    • Must fire whenever the LSP client receives a notification with a method that has been subscribed to through EditorApi.subscribeServerNotifications.

      Parameters

      • method: string
      • params: any

      Returns Promise<void>

    • Must be called exactly once on initialization with the current cursor position.

      Parameters

      Returns Promise<void>

    • Must fire whenever the user requests that the infoview perform an action.

      Parameters

      Returns Promise<void>

    • Execute the given JavaScript code inside the infoview. Must not be used for anything other than testing.

      Parameters

      • javaScript: string

      Returns Promise<void>

    • Like gotServerNotification, but fires on subscribed client->server notifications.

      Parameters

      • method: string
      • params: any

      Returns Promise<void>

    • Must fire with the server's message when the server is stopped.

      Parameters

      Returns Promise<void>

    Settings
    Member Visibility

    On This Page
    Methods