# HG changeset patch
# User wenzelm
# Date 1582724623 -3600
# Node ID ecefde4f910387684fcfffc677eb957c0da3e682
# Parent  7a867a38712a283e75ec35e9ab12145fd28b56f7
proper message passing -- discontinued obsolete auxiliary commands;

diff -r 7a867a38712a -r ecefde4f9103 src/Pure/build-jars
--- 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
diff -r 7a867a38712a -r ecefde4f9103 src/Tools/VSCode/extension/src/extension.ts
--- 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))
 
diff -r 7a867a38712a -r ecefde4f9103 src/Tools/VSCode/extension/src/state_panel.ts
--- 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) }
-}
diff -r 7a867a38712a -r ecefde4f9103 src/Tools/VSCode/src/state_panel.scala
--- 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 =
diff -r 7a867a38712a -r ecefde4f9103 src/Tools/VSCode/src/vscode_javascript.scala
--- 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://")
-}
-"""
-}