--- a/src/Pure/build-jars Tue Feb 25 21:28:06 2020 +0100
+++ b/src/Pure/build-jars Wed Feb 26 14:43:43 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/src/extension.ts Tue Feb 25 21:28:06 2020 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed Feb 26 14:43:43 2020 +0100
@@ -130,10 +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))
+ commands.registerCommand("isabelle.state", uri => state_panel.init(uri)))
language_client.onReady().then(() => state_panel.setup(context, language_client))
--- a/src/Tools/VSCode/extension/src/state_panel.ts Tue Feb 25 21:28:06 2020 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Wed Feb 26 14:43:43 2020 +0100
@@ -10,12 +10,17 @@
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 get_id(): number { return this.state_id }
public check_id(id: number): boolean { return this.state_id == id }
public set_content(id: number, html: string)
@@ -24,32 +29,41 @@
this.webview_panel.webview.html = html
}
- constructor(column: ViewColumn)
+ public reveal()
+ {
+ this.webview_panel.reveal(panel_column())
+ }
+
+ constructor()
{
this.webview_panel =
- window.createWebviewPanel("isabelle-state", "State", column,
+ window.createWebviewPanel("isabelle-state", "State", panel_column(),
{
enableScripts: true,
enableCommandUris: true,
retainContextWhenHidden: true,
});
this.webview_panel.onDidDispose(exit_panel)
- }
-
- public locate()
- {
- language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
- }
+ 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;
- public update()
- {
- language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
- }
+ case 'update':
+ language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+ break;
- public auto_update(enabled: boolean)
- {
- language_client.sendNotification(
- protocol.state_auto_update_type, { id: this.state_id, enabled: enabled })
+ case 'locate':
+ language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+ break;
+
+ default:
+ break;
+ }
+ })
}
}
@@ -71,31 +85,18 @@
}
}
+export function init(uri: Uri)
+{
+ if (panel) panel.reveal()
+ else language_client.sendNotification(protocol.state_init_type)
+}
+
export function setup(context: ExtensionContext, client: LanguageClient)
{
language_client = client
language_client.onNotification(protocol.state_output_type, params =>
{
- if (!panel) {
- const column = library.adjacent_editor_column(window.activeTextEditor, true)
- panel = new Panel(column)
- }
+ if (!panel) { panel = new Panel() }
panel.set_content(params.id, params.content)
})
}
-
-
-/* commands */
-
-export function init(uri: Uri) {
- language_client.sendNotification(protocol.state_init_type)
-}
-
-export function locate(id: number) { if (check_panel(id)) panel.locate() }
-
-export function update(id: number) { if (check_panel(id)) panel.update() }
-
-export function auto_update(id: number, enabled: boolean)
-{
- if (check_panel(id)) { panel.auto_update(enabled) }
-}
--- a/src/Tools/VSCode/src/state_panel.scala Tue Feb 25 21:28:06 2020 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala Wed Feb 26 14:43:43 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 Tue Feb 25 21:28:06 2020 +0100
+++ /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://")
-}
-"""
-}