See https://code.visualstudio.com/api/extension-guides/webview -- this is relevant for existing State output (broken in Isabelle2019), and might open possibilities for more advanced HTML displays.
Description
Description
Related Objects
Related Objects
Event Timeline
Comment Actions
Here is a proposed change:
# HG changeset patch # User XYZ # Date 1573057691 -3600 # Wed Nov 06 17:28:11 2019 +0100 # Node ID ec7c536b2b7ab516541f31e5a5be93d7391c27a1 # Parent b3956a37c99476571bfda9312da927dfdfdcb6b1 replaced previewHtml with WebviewPanel (previewHtml is no longer supported in latest vscode versions) diff -r b3956a37c994 -r ec7c536b2b7a src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Wed Nov 06 16:38:58 2019 +0100 +++ b/src/Tools/VSCode/extension/package.json Wed Nov 06 17:28:11 2019 +0100 @@ -17,7 +17,7 @@ "url": "https://isabelle.in.tum.de/repos/isabelle" }, "engines": { - "vscode": "^1.8.0" + "vscode": "^1.32.0" }, "categories": [ "Languages" @@ -317,7 +317,7 @@ "@types/node": "^7.0.66", "mocha": "^3.5.3", "typescript": "^2.9.2", - "vscode": "^1.1.18" + "vscode": "^1.1.36" }, "dependencies": { "vscode-languageclient": "~3.2.2" diff -r b3956a37c994 -r ec7c536b2b7a src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Wed Nov 06 16:38:58 2019 +0100 +++ b/src/Tools/VSCode/extension/src/preview.ts Wed Nov 06 17:28:11 2019 +0100 @@ -3,7 +3,7 @@ import * as timers from 'timers' import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position, workspace, - window, commands } from 'vscode' + window, commands, WebviewPanel } from 'vscode' import { LanguageClient } from 'vscode-languageclient'; import * as library from './library' import * as protocol from './protocol' @@ -39,22 +39,22 @@ { context.subscriptions.push(content_provider.register()) + var panel: WebviewPanel language_client = client language_client.onNotification(protocol.preview_response_type, params => { const preview_uri = encode_preview(Uri.parse(params.uri)) - if (preview_uri) { - content_provider.set_content(preview_uri, params.content) - content_provider.update(preview_uri) - - const existing_document = - workspace.textDocuments.find(document => - document.uri.scheme === preview_uri.scheme && - document.uri.query === preview_uri.query) - if (!existing_document && params.column != 0) { - commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label) - } + if (!panel) { + panel =window.createWebviewPanel( + preview_uri.fsPath, + params.label, + params.column, { + enableScripts: true, + retainContextWhenHidden: true + } + ); } + panel.webview.html = params.content; }) } diff -r b3956a37c994 -r ec7c536b2b7a src/Tools/VSCode/extension/src/preview_panel.ts --- a/src/Tools/VSCode/extension/src/preview_panel.ts Wed Nov 06 16:38:58 2019 +0100 +++ b/src/Tools/VSCode/extension/src/preview_panel.ts Wed Nov 06 17:28:11 2019 +0100 @@ -3,7 +3,7 @@ import * as timers from 'timers' import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position, workspace, - window, commands } from 'vscode' + window, commands, WebviewPanel } from 'vscode' import { LanguageClient } from 'vscode-languageclient'; import * as library from './library' import * as protocol from './protocol' @@ -39,22 +39,22 @@ { context.subscriptions.push(content_provider.register()) + var panel: WebviewPanel language_client = client language_client.onNotification(protocol.preview_response_type, params => { const preview_uri = encode_preview(Uri.parse(params.uri)) - if (preview_uri) { - content_provider.set_content(preview_uri, params.content) - content_provider.update(preview_uri) - - const existing_document = - workspace.textDocuments.find(document => - document.uri.scheme === preview_uri.scheme && - document.uri.query === preview_uri.query) - if (!existing_document && params.column != 0) { - commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label) - } + if (!panel) { + panel = window.createWebviewPanel( + preview_uri.fsPath, + params.label, + params.column, { + enableScripts: true, + retainContextWhenHidden: true + } + ); } + panel.webview.html = params.content; }) } diff -r b3956a37c994 -r ec7c536b2b7a src/Tools/VSCode/extension/src/state_panel.ts --- a/src/Tools/VSCode/extension/src/state_panel.ts Wed Nov 06 16:38:58 2019 +0100 +++ b/src/Tools/VSCode/extension/src/state_panel.ts Wed Nov 06 17:28:11 2019 +0100 @@ -3,8 +3,8 @@ import * as library from './library' import * as protocol from './protocol' import { Content_Provider } from './content_provider' -import { LanguageClient } from 'vscode-languageclient'; -import { Uri, ExtensionContext, workspace, commands, window } from 'vscode' +import { LanguageClient, VersionedTextDocumentIdentifier } from 'vscode-languageclient'; +import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel } from 'vscode' /* HTML content */ @@ -34,23 +34,23 @@ { context.subscriptions.push(content_provider.register()) + var panel: WebviewPanel language_client = client language_client.onNotification(protocol.state_output_type, params => { const uri = encode_state(params.id) - if (uri) { - content_provider.set_content(uri, params.content) - content_provider.update(uri) - - const existing_document = - workspace.textDocuments.find(document => - document.uri.scheme === uri.scheme && - document.uri.fragment === uri.fragment) - if (!existing_document) { - const column = library.adjacent_editor_column(window.activeTextEditor, true) - commands.executeCommand("vscode.previewHtml", uri, column, "State") - } + if (!panel) { + const column = library.adjacent_editor_column(window.activeTextEditor, true) + panel = window.createWebviewPanel( + uri.fsPath, + "State", + column, { + enableScripts: true, + retainContextWhenHidden: true + } + ); } + panel.webview.html = params.content; }) }