--- a/CONTRIBUTORS Tue Feb 25 17:37:22 2020 +0100
+++ b/CONTRIBUTORS Tue Feb 25 18:30:08 2020 +0100
@@ -17,6 +17,9 @@
Traytel
Extension of lift_bnf to support quotient types.
+* November 2019: Peter Zeller, TU Kaiserslautern
+ Update of Isabelle/VSCode to WebviewPanel API.
+
* October..December 2019: Makarius Wenzel
Isabelle/Phabrictor server setup, including Linux platform support in
Isabelle/Scala. Client-side tool "isabelle hg_setup".
--- a/NEWS Tue Feb 25 17:37:22 2020 +0100
+++ b/NEWS Tue Feb 25 18:30:08 2020 +0100
@@ -65,6 +65,11 @@
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
+*** Isabelle/VSCode Prover IDE ***
+
+* Update to WebviewPanel API.
+
+
*** HOL ***
* Improvements of the 'lift_bnf' command:
--- a/src/Tools/VSCode/extension/package.json Tue Feb 25 17:37:22 2020 +0100
+++ b/src/Tools/VSCode/extension/package.json Tue Feb 25 18:30:08 2020 +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"
--- a/src/Tools/VSCode/extension/src/preview.ts Tue Feb 25 17:37:22 2020 +0100
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue Feb 25 18:30:08 2020 +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,23 @@
{
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;
})
}
--- a/src/Tools/VSCode/extension/src/preview_panel.ts Tue Feb 25 17:37:22 2020 +0100
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts Tue Feb 25 18:30:08 2020 +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,23 @@
{
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;
})
}
--- a/src/Tools/VSCode/extension/src/state_panel.ts Tue Feb 25 17:37:22 2020 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Tue Feb 25 18:30:08 2020 +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,24 @@
{
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;
})
}