diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 6f1b0a3b..6129762f 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -9,6 +9,7 @@ import { checkAll, SetupDiagnostics } from './diagnostics/setupDiagnostics' import { PreconditionCheckResult, SetupNotificationOptions } 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' @@ -195,7 +196,7 @@ async function activateLean4Features( watchService.lakeFileChanged(packageUri => installer.handleLakeFileChanged(packageUri)) context.subscriptions.push(watchService) - const infoProvider = new InfoProvider(clientProvider, 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 0bace229..0e1e8f9a 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -9,12 +9,12 @@ import { ServerStoppedReason, TextInsertKind, } from '@leanprover/infoview-api' -import { join } from 'path' import { commands, Diagnostic, Disposable, env, + Event, ExtensionContext, Position, Range, @@ -22,7 +22,7 @@ import { TextEditor, TextEditorRevealType, Uri, - WebviewPanel, + ViewColumn, window, workspace, } from 'vscode' @@ -40,8 +40,6 @@ import { getInfoViewShowGoalNames, getInfoViewShowTooltipOnHover, getInfoViewStyle, - minIfProd, - prodOrDev, } from './config' import { LeanClient } from './leanclient' import { Rpc } from './rpc' @@ -53,6 +51,19 @@ import { logger } from './utils/logger' import { displayNotification } from './utils/notifs' import { viewColumnOfActiveTextEditor, viewColumnOfInfoView } from './utils/viewColumn' +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 { @@ -90,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[] = [] @@ -320,6 +331,7 @@ export class InfoProvider implements Disposable { constructor( private clientProvider: LeanClientProvider, private context: ExtensionContext, + private infoWebviewFactory: InfoWebviewFactory, ) { this.updateStylesheet() @@ -582,48 +594,13 @@ export class InfoProvider implements Disposable { if (this.webviewPanel) { this.webviewPanel.reveal(undefined, true) } else { - const webviewPanel = window.createWebviewPanel( - 'lean4_infoview', - 'Lean Infoview', - { viewColumn: viewColumnOfInfoView(), 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() + const webviewPanel = this.infoWebviewFactory.make(this.editorApi, this.stylesheet) 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(leanEditor.documentExtUri) await this.initInfoView(leanEditor, client) @@ -819,35 +796,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..cf7719e2 --- /dev/null +++ b/vscode-lean4/src/infowebview.ts @@ -0,0 +1,97 @@ +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' +import { viewColumnOfInfoView } from './utils/viewColumn' + + +export class VSCodeInfoWebviewFactory implements InfoWebviewFactory { + constructor(private context: ExtensionContext) {} + + make(editorApi: EditorApi, stylesheet: string) { + const webviewPanel = window.createWebviewPanel( + 'lean4_infoview', + 'Lean Infoview', + { viewColumn: viewColumnOfInfoView(), 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 + + + + +
+ + + ` + } +}