--- a/CONTRIBUTORS Wed Feb 26 12:21:48 2020 +0000
+++ b/CONTRIBUTORS Wed Feb 26 16:08:05 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 Wed Feb 26 12:21:48 2020 +0000
+++ b/NEWS Wed Feb 26 16:08:05 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/Pure/build-jars Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Pure/build-jars Wed Feb 26 16:08:05 2020 +0100
@@ -196,7 +196,6 @@
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/state_panel.scala
- src/Tools/VSCode/src/vscode_javascript.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/VSCode/src/vscode_spell_checker.scala
--- a/src/Tools/VSCode/extension/package.json Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/package.json Wed Feb 26 16:08:05 2020 +0100
@@ -10,25 +10,24 @@
"document preparation"
],
"icon": "isabelle.png",
- "version": "1.1.2",
+ "version": "1.2.0",
"publisher": "makarius",
"license": "MIT",
"repository": {
- "url": "https://isabelle.in.tum.de/repos/isabelle"
+ "url": "https://isabelle-dev.sketis.net"
},
"engines": {
- "vscode": "^1.8.0"
+ "vscode": "^1.32.0"
},
"categories": [
- "Languages"
+ "Programming Languages"
],
"activationEvents": [
"onLanguage:isabelle",
"onLanguage:isabelle-ml",
"onLanguage:bibtex",
"onCommand:isabelle.preview",
- "onCommand:isabelle.preview-split",
- "onCommand:isabelle.preview-source"
+ "onCommand:isabelle.preview-split"
],
"main": "./out/src/extension",
"contributes": {
@@ -48,15 +47,6 @@
}
},
{
- "command": "isabelle.preview-update",
- "title": "Update Preview",
- "category": "Isabelle",
- "icon": {
- "light": "./media/Preview.svg",
- "dark": "./media/Preview_inverse.svg"
- }
- },
- {
"command": "isabelle.preview-split",
"title": "Open Preview (Split Editor)",
"category": "Isabelle",
@@ -66,15 +56,6 @@
}
},
{
- "command": "isabelle.preview-source",
- "title": "Show Source",
- "category": "Isabelle",
- "icon": {
- "light": "./media/ViewSource.svg",
- "dark": "./media/ViewSource_inverse.svg"
- }
- },
- {
"command": "isabelle.include-word",
"title": "Include word",
"category": "Isabelle"
@@ -131,16 +112,6 @@
"when": "editorLangId == bibtex",
"command": "isabelle.preview-split",
"group": "navigation"
- },
- {
- "when": "resourceScheme == isabelle-preview",
- "command": "isabelle.preview-update",
- "group": "navigation"
- },
- {
- "when": "resourceScheme == isabelle-preview",
- "command": "isabelle.preview-source",
- "group": "navigation"
}
],
"explorer/context": [
@@ -317,7 +288,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/content_provider.ts Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-'use strict'
-
-import { Event, EventEmitter, Uri, TextDocumentContentProvider, Disposable,
- workspace } from 'vscode'
-
-
-export class Content_Provider implements TextDocumentContentProvider
-{
- private _uri_template: Uri
- get uri_template(): Uri { return this._uri_template }
- get uri_scheme(): string { return this.uri_template.scheme }
-
- constructor(uri_scheme: string)
- {
- this._uri_template = Uri.parse("scheme:").with({ scheme: uri_scheme })
- }
- dispose() { }
-
- private emitter = new EventEmitter<Uri>()
- public update(uri: Uri) { this.emitter.fire(uri) }
- get onDidChange(): Event<Uri> { return this.emitter.event }
-
- private content = new Map<string, string>()
- public set_content(uri: Uri, content: string) { this.content.set(uri.toString(), content)}
-
- provideTextDocumentContent(uri: Uri): string
- {
- return this.content.get(uri.toString()) || ""
- }
-
- public register(): Disposable
- {
- return workspace.registerTextDocumentContentProvider(this.uri_scheme, this)
- }
-}
--- a/src/Tools/VSCode/extension/src/extension.ts Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed Feb 26 16:08:05 2020 +0100
@@ -130,11 +130,7 @@
/* state panel */
context.subscriptions.push(
- commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
- commands.registerCommand("_isabelle.state-locate", state_panel.locate),
- commands.registerCommand("_isabelle.state-update", state_panel.update),
- commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update),
- workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri)))
+ commands.registerCommand("isabelle.state", uri => state_panel.init(uri)))
language_client.onReady().then(() => state_panel.setup(context, language_client))
@@ -143,9 +139,7 @@
context.subscriptions.push(
commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
- commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
- commands.registerCommand("isabelle.preview-source", preview_panel.source),
- commands.registerCommand("isabelle.preview-update", preview_panel.update))
+ commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)))
language_client.onReady().then(() => preview_panel.setup(context, language_client))
--- a/src/Tools/VSCode/extension/src/preview.ts Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-'use strict';
-
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
- ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
- window, commands } from 'vscode'
-import { LanguageClient } from 'vscode-languageclient';
-import * as library from './library'
-import * as protocol from './protocol'
-import { Content_Provider } from './content_provider'
-
-
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-preview")
-
-function encode_preview(document_uri: Uri | undefined): Uri | undefined
-{
- if (document_uri && library.is_file(document_uri)) {
- return content_provider.uri_template.with({ query: document_uri.fsPath })
- }
- else undefined
-}
-
-function decode_preview(preview_uri: Uri | undefined): Uri | undefined
-{
- if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
- return Uri.file(preview_uri.query)
- }
- else undefined
-}
-
-
-/* setup */
-
-let language_client: LanguageClient
-
-export function setup(context: ExtensionContext, client: LanguageClient)
-{
- context.subscriptions.push(content_provider.register())
-
- 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)
- }
- }
- })
-}
-
-
-/* commands */
-
-export function request(uri?: Uri, split: boolean = false)
-{
- const document_uri = uri || window.activeTextEditor.document.uri
- const preview_uri = encode_preview(document_uri)
- if (preview_uri && language_client) {
- language_client.sendNotification(protocol.preview_request_type,
- { uri: document_uri.toString(),
- column: library.adjacent_editor_column(window.activeTextEditor, split) })
- }
-}
-
-export function update(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri && language_client) {
- language_client.sendNotification(protocol.preview_request_type,
- { uri: document_uri.toString(), column: 0 })
- }
-}
-
-export function source(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri) {
- const editor =
- window.visibleTextEditors.find(editor =>
- library.is_file(editor.document.uri) &&
- editor.document.uri.fsPath === document_uri.fsPath)
- if (editor) window.showTextDocument(editor.document, editor.viewColumn)
- else workspace.openTextDocument(document_uri).then(window.showTextDocument)
- }
- else commands.executeCommand("workbench.action.navigateBack")
-}
--- a/src/Tools/VSCode/extension/src/preview_panel.ts Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts Wed Feb 26 16:08:05 2020 +0100
@@ -1,93 +1,59 @@
'use strict';
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
- ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
- window, commands } from 'vscode'
+import { ExtensionContext, Uri, workspace,
+ window, commands, ViewColumn, WebviewPanel } from 'vscode'
import { LanguageClient } from 'vscode-languageclient';
import * as library from './library'
import * as protocol from './protocol'
-import { Content_Provider } from './content_provider'
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-preview")
-
-function encode_preview(document_uri: Uri | undefined): Uri | undefined
-{
- if (document_uri && library.is_file(document_uri)) {
- return content_provider.uri_template.with({ query: document_uri.fsPath })
- }
- else undefined
-}
-
-function decode_preview(preview_uri: Uri | undefined): Uri | undefined
-{
- if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
- return Uri.file(preview_uri.query)
- }
- else undefined
-}
-
-
-/* setup */
-
let language_client: LanguageClient
+class Panel
+{
+ private webview_panel: WebviewPanel
+
+ public set_content(title: string, body: string)
+ {
+ this.webview_panel.title = title
+ this.webview_panel.webview.html = body
+ }
+
+ public reveal(column: ViewColumn)
+ {
+ this.webview_panel.reveal(column)
+ }
+
+ constructor(column: ViewColumn)
+ {
+ this.webview_panel =
+ window.createWebviewPanel("isabelle-preview", "Preview", column,
+ {
+ enableScripts: true
+ });
+ this.webview_panel.onDidDispose(() => { panel = null })
+ }
+}
+
+let panel: Panel
+
export function setup(context: ExtensionContext, client: LanguageClient)
{
- context.subscriptions.push(content_provider.register())
-
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 = new Panel(params.column) }
+ else panel.reveal(params.column)
+ panel.set_content(params.label, params.content)
})
}
-
-/* commands */
-
export function request(uri?: Uri, split: boolean = false)
{
const document_uri = uri || window.activeTextEditor.document.uri
- const preview_uri = encode_preview(document_uri)
- if (preview_uri && language_client) {
+ if (language_client) {
language_client.sendNotification(protocol.preview_request_type,
{ uri: document_uri.toString(),
column: library.adjacent_editor_column(window.activeTextEditor, split) })
}
}
-
-export function update(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri && language_client) {
- language_client.sendNotification(protocol.preview_request_type,
- { uri: document_uri.toString(), column: 0 })
- }
-}
-
-export function source(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri) {
- const editor = library.find_file_editor(document_uri)
- if (editor) window.showTextDocument(editor.document, editor.viewColumn)
- else workspace.openTextDocument(document_uri).then(window.showTextDocument)
- }
- else commands.executeCommand("workbench.action.navigateBack")
-}
--- a/src/Tools/VSCode/extension/src/state_panel.ts Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Wed Feb 26 16:08:05 2020 +0100
@@ -2,89 +2,91 @@
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'
-
-
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-state")
+import { Uri, ExtensionContext, window, WebviewPanel, ViewColumn } from 'vscode'
-function encode_state(id: number | undefined): Uri | undefined
-{
- return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined
-}
-
-function decode_state(uri: Uri | undefined): number | undefined
-{
- if (uri && uri.scheme === content_provider.uri_scheme) {
- const id = parseInt(uri.fragment)
- return id ? id : undefined
- }
- else undefined
-}
-
-
-/* setup */
let language_client: LanguageClient
+function panel_column(): ViewColumn
+{
+ return library.adjacent_editor_column(window.activeTextEditor, true)
+}
+
+class Panel
+{
+ private state_id: number
+ private webview_panel: WebviewPanel
+
+ public get_id(): number { return this.state_id }
+ public check_id(id: number): boolean { return this.state_id == id }
+
+ public set_content(id: number, body: string)
+ {
+ this.state_id = id
+ this.webview_panel.webview.html = body
+ }
+
+ public reveal()
+ {
+ this.webview_panel.reveal(panel_column())
+ }
+
+ constructor()
+ {
+ this.webview_panel =
+ window.createWebviewPanel("isabelle-state", "State", panel_column(),
+ {
+ enableScripts: true
+ });
+ this.webview_panel.onDidDispose(exit_panel)
+ this.webview_panel.webview.onDidReceiveMessage(message =>
+ {
+ switch (message.command) {
+ case 'auto_update':
+ language_client.sendNotification(
+ protocol.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
+ break;
+
+ case 'update':
+ language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+ break;
+
+ case 'locate':
+ language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+ break;
+
+ default:
+ break;
+ }
+ })
+ }
+}
+
+let panel: Panel
+
+function exit_panel()
+{
+ if (panel) {
+ language_client.sendNotification(protocol.state_exit_type, { id: panel.get_id() })
+ panel = null
+ }
+}
+
+export function init(uri: Uri)
+{
+ if (language_client) {
+ if (panel) panel.reveal()
+ else language_client.sendNotification(protocol.state_init_type)
+ }
+}
+
export function setup(context: ExtensionContext, client: LanguageClient)
{
- context.subscriptions.push(content_provider.register())
-
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) { panel = new Panel() }
+ panel.set_content(params.id, params.content)
})
}
-
-
-/* commands */
-
-export function init(uri: Uri)
-{
- if (language_client) language_client.sendNotification(protocol.state_init_type)
-}
-
-export function exit(id: number)
-{
- if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
-}
-
-export function exit_uri(uri: Uri)
-{
- const id = decode_state(uri)
- if (id) exit(id)
-}
-
-export function locate(id: number)
-{
- if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
-}
-
-export function update(id: number)
-{
- if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
-}
-
-export function auto_update(id: number, enabled: boolean)
-{
- if (language_client)
- language_client.sendNotification(protocol.state_auto_update_type, { id: id, enabled: enabled })
-}
--- a/src/Tools/VSCode/src/state_panel.scala Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/src/state_panel.scala Wed Feb 26 16:08:05 2020 +0100
@@ -109,14 +109,17 @@
/* controls */
private def controls_script =
- VSCode_JavaScript.invoke_command +
"""
+const vscode = acquireVsCodeApi();
+
function invoke_auto_update(enabled)
-{ invoke_command("_isabelle.state-auto-update", [""" + id + """, enabled]) }
+{ vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) }
-function invoke_update() { invoke_command("_isabelle.state-update", [""" + id + """]) }
+function invoke_update()
+{ vscode.postMessage({'command': 'update'}) }
-function invoke_locate() { invoke_command("_isabelle.state-locate", [""" + id + """]) }
+function invoke_locate()
+{ vscode.postMessage({'command': 'locate'}) }
"""
private def auto_update_button: XML.Elem =
--- a/src/Tools/VSCode/src/vscode_javascript.scala Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-/* Title: Tools/VSCode/src/vscode_javascript.scala
- Author: Makarius
-
-JavaScript snippets for VSCode HTML view.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-
-object VSCode_JavaScript
-{
- val invoke_command =
-"""
-function invoke_command(name, args)
-{
- window.parent.postMessage(
- {
- command: "did-click-link",
- data: "command:" + encodeURIComponent(name) + "?" + encodeURIComponent(JSON.stringify(args))
- }, "file://")
-}
-"""
-}