# HG changeset patch # User wenzelm # Date 1645188530 -3600 # Node ID faa24820fba15b2bb79b24e33b5ee1dec9d6b53f # Parent 81a858c3cb5b03478202325b5d506523c56496ba tuned; diff -r 81a858c3cb5b -r faa24820fba1 src/Tools/VSCode/extension/src/preview_panel.ts --- a/src/Tools/VSCode/extension/src/preview_panel.ts Fri Feb 18 13:26:36 2022 +0100 +++ b/src/Tools/VSCode/extension/src/preview_panel.ts Fri Feb 18 13:48:50 2022 +0100 @@ -1,8 +1,7 @@ 'use strict'; -import { ExtensionContext, Uri, workspace, - window, commands, ViewColumn, WebviewPanel } from 'vscode' -import { LanguageClient } from 'vscode-languageclient'; +import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode' +import { LanguageClient } from 'vscode-languageclient' import * as library from './library' import * as protocol from './protocol' @@ -30,7 +29,7 @@ window.createWebviewPanel("isabelle-preview", "Preview", column, { enableScripts: true - }); + }) this.webview_panel.onDidDispose(() => { panel = null }) } }