From 50bf3b495462b5cfde955987c4464fff05453067 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 4 Nov 2024 14:17:36 +0100 Subject: [PATCH 1/2] feat: detachable infoview --- vscode-lean4/webview/index.ts | 78 +++++++++++++++++++++++++++++++++-- 1 file changed, 75 insertions(+), 3 deletions(-) diff --git a/vscode-lean4/webview/index.ts b/vscode-lean4/webview/index.ts index a0625c893..2346ad239 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) + } + } + }) } From 96dd323fed274e4da18d075446c0127942c8c1cc Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 4 Nov 2024 14:21:56 +0100 Subject: [PATCH 2/2] refactor: style --- vscode-lean4/webview/index.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/vscode-lean4/webview/index.ts b/vscode-lean4/webview/index.ts index 2346ad239..7f03fcc75 100644 --- a/vscode-lean4/webview/index.ts +++ b/vscode-lean4/webview/index.ts @@ -8,16 +8,16 @@ import { Rpc } from '../src/rpc' // 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 { +interface PersistentInfoviewState { config?: InfoviewConfig cursorLoc?: Location initializeResult?: InitializeResult diags?: PublishDiagnosticsParams } -const vscodeApi = acquireVsCodeApi() +const vscodeApi = acquireVsCodeApi() -function modifyState(f: (previousState: PersistentInfoViewState) => PersistentInfoViewState) { +function modifyState(f: (previousState: PersistentInfoviewState) => PersistentInfoviewState) { vscodeApi.setState(f(vscodeApi.getState() ?? {})) } @@ -35,7 +35,7 @@ if (div && script) { 'react-dom': script.getAttribute('data-importmap-react-dom')!, } loadRenderInfoview(imports, [editorApi, div], async api => { - const previousState: PersistentInfoViewState | undefined = vscodeApi.getState() + const previousState: PersistentInfoviewState | undefined = vscodeApi.getState() const apiWithPersistedState: InfoviewApi = { ...api } apiWithPersistedState.initialize = async loc => {