From 6dcb094528eefe962d3864878de9286c016bee26 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Sat, 6 Jul 2024 10:00:06 +0200 Subject: [PATCH] feat: [lean4web] abstract the implementation of the infoview as a webview --- vscode-lean4/src/extension.ts | 8 ++- vscode-lean4/src/infoview.ts | 93 +++++++------------------------- vscode-lean4/src/infowebview.ts | 95 +++++++++++++++++++++++++++++++++ 3 files changed, 120 insertions(+), 76 deletions(-) create mode 100644 vscode-lean4/src/infowebview.ts diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index dcb09575..d3c33a1e 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -15,6 +15,7 @@ import { import { PreconditionCheckResult } from './diagnostics/setupNotifs' import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports' import { InfoProvider } from './infoview' +import { VSCodeInfoWebviewFactory } from './infowebview' import { LeanClient } from './leanclient' import { LoogleView } from './loogleview' import { ManualView } from './manualview' @@ -187,7 +188,12 @@ async function activateLean4Features( watchService.lakeFileChanged(packageUri => installer.handleLakeFileChanged(packageUri)) context.subscriptions.push(watchService) - const infoProvider = new InfoProvider(clientProvider, { language: 'lean4' }, context) + const infoProvider = new InfoProvider( + clientProvider, + { language: 'lean4' }, + context, + new VSCodeInfoWebviewFactory(context), + ) context.subscriptions.push(infoProvider) context.subscriptions.push(new LeanTaskGutter(clientProvider, context)) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 80dd4186..6f41b663 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -9,13 +9,13 @@ import { ServerStoppedReason, TextInsertKind, } from '@leanprover/infoview-api' -import { join } from 'path' import { commands, Diagnostic, Disposable, DocumentSelector, env, + Event, ExtensionContext, languages, Position, @@ -25,7 +25,6 @@ import { TextEditorRevealType, Uri, ViewColumn, - WebviewPanel, window, workspace, } from 'vscode' @@ -43,8 +42,6 @@ import { getInfoViewShowGoalNames, getInfoViewShowTooltipOnHover, getInfoViewStyle, - minIfProd, - prodOrDev, } from './config' import { LeanClient } from './leanclient' import { Rpc } from './rpc' @@ -54,6 +51,19 @@ import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' import { logger } from './utils/logger' import { displayError, displayInformation } from './utils/notifs' +export interface InfoWebview { + readonly api: InfoviewApi + readonly rpc: Rpc + readonly visible: boolean + dispose(): any + reveal(viewColumn?: ViewColumn, preserveFocus?: boolean): void + onDidDispose: Event +} + +export interface InfoWebviewFactory { + make(editorApi: EditorApi, stylesheet: string, column: number): InfoWebview +} + const keepAlivePeriodMs = 10000 async function rpcConnect(client: LeanClient, uri: ls.DocumentUri): Promise { @@ -91,7 +101,7 @@ class RpcSessionAtPos implements Disposable { export class InfoProvider implements Disposable { /** Instance of the panel, if it is open. Otherwise `undefined`. */ - private webviewPanel?: WebviewPanel & { rpc: Rpc; api: InfoviewApi } + private webviewPanel?: InfoWebview private subscriptions: Disposable[] = [] private clientSubscriptions: Disposable[] = [] @@ -332,6 +342,7 @@ export class InfoProvider implements Disposable { private provider: LeanClientProvider, private readonly leanDocs: DocumentSelector, private context: ExtensionContext, + private infoWebviewFactory: InfoWebviewFactory, ) { this.clientProvider = provider this.updateStylesheet() @@ -605,49 +616,12 @@ export class InfoProvider implements Disposable { if (this.webviewPanel) { this.webviewPanel.reveal(column, true) } else { - const webviewPanel = window.createWebviewPanel( - 'lean4_infoview', - 'Lean Infoview', - { viewColumn: column, preserveFocus: true }, - { - enableFindWidget: true, - retainContextWhenHidden: true, - enableScripts: true, - enableCommandUris: true, - }, - ) as WebviewPanel & { rpc: Rpc; api: InfoviewApi } - - // Note that an extension can send data to its webviews using webview.postMessage(). - // This method sends any JSON serializable data to the webview. The message is received - // inside the webview through the standard message event. - // The receiving of these messages is done inside webview\index.ts where it - // calls window.addEventListener('message',... - webviewPanel.rpc = new Rpc(m => { - try { - void webviewPanel.webview.postMessage(m) - } catch (e) { - // ignore any disposed object exceptions - } - }) - webviewPanel.rpc.register(this.editorApi) - - // Similarly, we can received data from the webview by listening to onDidReceiveMessage. - webviewPanel.webview.onDidReceiveMessage(m => { - try { - webviewPanel.rpc.messageReceived(m) - } catch { - // ignore any disposed object exceptions - } - }) - webviewPanel.api = webviewPanel.rpc.getApi() - webviewPanel.onDidDispose(() => { + this.webviewPanel = this.infoWebviewFactory.make(this.editorApi, this.stylesheet, column) + this.webviewPanel.onDidDispose(() => { this.webviewPanel = undefined this.clearNotificationHandlers() this.clearRpcSessions(null) // should be after `webviewPanel = undefined` }) - this.webviewPanel = webviewPanel - webviewPanel.webview.html = this.initialHtml() - const client = this.clientProvider.findClient(docUri) await this.initInfoView(editor, client) } @@ -862,35 +836,4 @@ export class InfoProvider implements Disposable { // ensure the text document has the keyboard focus. await window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false }) } - - private getLocalPath(path: string): string | undefined { - if (this.webviewPanel) { - return this.webviewPanel.webview.asWebviewUri(Uri.file(join(this.context.extensionPath, path))).toString() - } - return undefined - } - - private initialHtml() { - const libPostfix = `.${prodOrDev}${minIfProd}.js` - return ` - - - - - - Infoview - - - - -
- - - ` - } } diff --git a/vscode-lean4/src/infowebview.ts b/vscode-lean4/src/infowebview.ts new file mode 100644 index 00000000..5593804b --- /dev/null +++ b/vscode-lean4/src/infowebview.ts @@ -0,0 +1,95 @@ +import { EditorApi, InfoviewApi } from '@leanprover/infoview-api' +import { join } from 'path' +import { ExtensionContext, Uri, ViewColumn, WebviewPanel, window } from 'vscode' +import { minIfProd, prodOrDev } from './config' +import { InfoWebviewFactory } from './infoview' +import { Rpc } from './rpc' + +export class VSCodeInfoWebviewFactory implements InfoWebviewFactory { + constructor(private context: ExtensionContext) {} + + make(editorApi: EditorApi, stylesheet: string, column: number) { + const webviewPanel = window.createWebviewPanel( + 'lean4_infoview', + 'Lean Infoview', + { viewColumn: column, preserveFocus: true }, + { + enableFindWidget: true, + retainContextWhenHidden: true, + enableScripts: true, + enableCommandUris: true, + }, + ) + + // Note that an extension can send data to its webviews using webview.postMessage(). + // This method sends any JSON serializable data to the webview. The message is received + // inside the webview through the standard message event. + // The receiving of these messages is done inside webview\index.ts where it + // calls window.addEventListener('message',... + const rpc = new Rpc(m => { + try { + void webviewPanel.webview.postMessage(m) + } catch (e) { + // ignore any disposed object exceptions + } + }) + rpc.register(editorApi) + + // Similarly, we can received data from the webview by listening to onDidReceiveMessage. + webviewPanel.webview.onDidReceiveMessage(m => { + try { + rpc.messageReceived(m) + } catch { + // ignore any disposed object exceptions + } + }) + const api = rpc.getApi() + webviewPanel.webview.html = this.initialHtml(webviewPanel, stylesheet) + + return { + api, + rpc, + get visible() { + return webviewPanel.visible + }, + dispose: () => { + webviewPanel.dispose() + }, + reveal: (viewColumn?: ViewColumn, preserveFocus?: boolean) => { + webviewPanel.reveal(viewColumn, preserveFocus) + }, + onDidDispose: webviewPanel.onDidDispose, + } + } + + private getLocalPath(path: string, webviewPanel: WebviewPanel): string | undefined { + if (webviewPanel) { + return webviewPanel.webview.asWebviewUri(Uri.file(join(this.context.extensionPath, path))).toString() + } + return undefined + } + + private initialHtml(webviewPanel: WebviewPanel, stylesheet: string) { + const libPostfix = `.${prodOrDev}${minIfProd}.js` + return ` + + + + + + Infoview + + + + +
+ + + ` + } +}