feat: [lean4web] abstract the implementation of infoview as a webview

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))

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<void>
+}
+
+export interface InfoWebviewFactory {
+    make(editorApi: EditorApi, stylesheet: string, column: number): InfoWebview
+}
+
 const keepAlivePeriodMs = 10000
 
 async function rpcConnect(client: LeanClient, uri: ls.DocumentUri): Promise<string> {
@@ -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 `
-            <!DOCTYPE html>
-            <html>
-            <head>
-                <meta charset="UTF-8" />
-                <meta http-equiv="Content-type" content="text/html;charset=utf-8">
-                <title>Infoview</title>
-                <style>${this.stylesheet}</style>
-                <link rel="stylesheet" href="${this.getLocalPath('dist/lean4-infoview/index.css')}">
-            </head>
-            <body>
-                <div id="react_root"></div>
-                <script
-                    data-importmap-leanprover-infoview="${this.getLocalPath(`dist/lean4-infoview/index${libPostfix}`)}"
-                    data-importmap-react="${this.getLocalPath(`dist/lean4-infoview/react${libPostfix}`)}"
-                    data-importmap-react-jsx-runtime="${this.getLocalPath(`dist/lean4-infoview/react-jsx-runtime${libPostfix}`)}"
-                    data-importmap-react-dom="${this.getLocalPath(`dist/lean4-infoview/react-dom${libPostfix}`)}"
-                    src="${this.getLocalPath('dist/webview.js')}"></script>
-            </body>
-            </html>`
-    }
 }

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<InfoviewApi>()
+        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 `
+            <!DOCTYPE html>
+            <html>
+            <head>
+                <meta charset="UTF-8" />
+                <meta http-equiv="Content-type" content="text/html;charset=utf-8">
+                <title>Infoview</title>
+                <style>${stylesheet}</style>
+                <link rel="stylesheet" href="${this.getLocalPath('dist/lean4-infoview/index.css', webviewPanel)}">
+            </head>
+            <body>
+                <div id="react_root"></div>
+                <script
+                    data-importmap-leanprover-infoview="${this.getLocalPath(`dist/lean4-infoview/index${libPostfix}`, webviewPanel)}"
+                    data-importmap-react="${this.getLocalPath(`dist/lean4-infoview/react${libPostfix}`, webviewPanel)}"
+                    data-importmap-react-jsx-runtime="${this.getLocalPath(`dist/lean4-infoview/react-jsx-runtime${libPostfix}`, webviewPanel)}"
+                    data-importmap-react-dom="${this.getLocalPath(`dist/lean4-infoview/react-dom${libPostfix}`, webviewPanel)}"
+                    src="${this.getLocalPath('dist/webview.js', webviewPanel)}"></script>
+            </body>
+            </html>`
+    }
+}