diff --git a/vscode-lean4/webview/index.ts b/vscode-lean4/webview/index.ts index a0625c89..2346ad23 100644 --- a/vscode-lean4/webview/index.ts +++ b/vscode-lean4/webview/index.ts @@ -1,8 +1,25 @@ -import type { EditorApi } from '@leanprover/infoview' +import type { EditorApi, InfoviewApi, InfoviewConfig } from '@leanprover/infoview' import { loadRenderInfoview } from '@leanprover/infoview/loader' +import type { InitializeResult, Location, PublishDiagnosticsParams } from 'vscode-languageserver-protocol' import { Rpc } from '../src/rpc' -const vscodeApi = acquireVsCodeApi() +// Even when the Infoview is loaded in a webview panel with the `retainContextWhenHidden` set, +// when the Infoview is detached, it will be reset to its initial state. +// Persisting the most important state necessary for rendering the InfoView ensures that it +// can be rendered correctly when detaching it. +// We persist this state by intercepting the Infoview API and load it when this script is initialized. +export interface PersistentInfoViewState { + config?: InfoviewConfig + cursorLoc?: Location + initializeResult?: InitializeResult + diags?: PublishDiagnosticsParams +} + +const vscodeApi = acquireVsCodeApi() + +function modifyState(f: (previousState: PersistentInfoViewState) => PersistentInfoViewState) { + vscodeApi.setState(f(vscodeApi.getState() ?? {})) +} const rpc = new Rpc((m: any) => vscodeApi.postMessage(m)) window.addEventListener('message', e => rpc.messageReceived(e.data)) @@ -17,5 +34,60 @@ if (div && script) { 'react/jsx-runtime': script.getAttribute('data-importmap-react-jsx-runtime')!, 'react-dom': script.getAttribute('data-importmap-react-dom')!, } - loadRenderInfoview(imports, [editorApi, div], api => rpc.register(api)) + loadRenderInfoview(imports, [editorApi, div], async api => { + const previousState: PersistentInfoViewState | undefined = vscodeApi.getState() + + const apiWithPersistedState: InfoviewApi = { ...api } + apiWithPersistedState.initialize = async loc => { + await api.initialize(loc) + modifyState(s => { + return { ...s, cursorLoc: loc } + }) + } + apiWithPersistedState.changedCursorLocation = async loc => { + await api.changedCursorLocation(loc) + if (loc !== undefined) { + modifyState(s => { + return { ...s, cursorLoc: loc } + }) + } + } + apiWithPersistedState.changedInfoviewConfig = async config => { + await api.changedInfoviewConfig(config) + modifyState(s => { + return { ...s, config } + }) + } + apiWithPersistedState.serverRestarted = async initializeResult => { + await api.serverRestarted(initializeResult) + modifyState(s => { + return { ...s, initializeResult } + }) + } + apiWithPersistedState.gotServerNotification = async (method, params) => { + await api.gotServerNotification(method, params) + if (method === 'textDocument/publishDiagnostics') { + modifyState(s => { + return { ...s, diags: params } + }) + } + } + + rpc.register(apiWithPersistedState) + + if (previousState !== undefined) { + if (previousState.cursorLoc !== undefined) { + await api.initialize(previousState.cursorLoc) + } + if (previousState.config !== undefined) { + await api.changedInfoviewConfig(previousState.config) + } + if (previousState.initializeResult !== undefined) { + await api.serverRestarted(previousState.initializeResult) + } + if (previousState.diags !== undefined) { + await api.gotServerNotification('textDocument/publishDiagnostics', previousState.diags) + } + } + }) }