HTML GUI actions via JavaScript;

--- a/src/Pure/build-jars	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Pure/build-jars	Thu Jun 29 11:36:25 2017 +0200
@@ -172,6 +172,7 @@
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala
   ../Tools/VSCode/src/state_panel.scala
+  ../Tools/VSCode/src/vscode_javascript.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
   ../Tools/VSCode/src/vscode_spell_checker.scala

--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 11:36:25 2017 +0200
@@ -107,7 +107,8 @@
     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-update", state_panel.update),
+      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update))
 
     language_client.onReady().then(() => state_panel.setup(context, language_client))
 

--- a/src/Tools/VSCode/extension/src/protocol.ts	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Thu Jun 29 11:36:25 2017 +0200
@@ -63,10 +63,18 @@
   id: number
 }
 
+export interface Auto_Update
+{
+  id: number
+  enabled: boolean
+}
+
 export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
 export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
 export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
 export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
+export const state_auto_update_type =
+  new NotificationType<Auto_Update, void>("PIDE/state_auto_update")
 
 
 /* preview */

--- a/src/Tools/VSCode/extension/src/state_panel.ts	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Thu Jun 29 11:36:25 2017 +0200
@@ -76,3 +76,9 @@
 {
   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/protocol.scala	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 11:36:25 2017 +0200
@@ -528,6 +528,19 @@
   object State_Locate extends State_Id_Notification("PIDE/state_locate")
   object State_Update extends State_Id_Notification("PIDE/state_update")
 
+  object State_Auto_Update
+  {
+    def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] =
+      json match {
+        case Notification("PIDE/state_auto_update", Some(params)) =>
+          for {
+            id <- JSON.long(params, "id")
+            enabled <- JSON.bool(params, "enabled")
+          } yield (id, enabled)
+        case _ => None
+      }
+  }
+
 
   /* preview */
 

--- a/src/Tools/VSCode/src/server.scala	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Jun 29 11:36:25 2017 +0200
@@ -450,6 +450,7 @@
           case Protocol.State_Exit(id) => State_Panel.exit(id)
           case Protocol.State_Locate(id) => State_Panel.locate(id)
           case Protocol.State_Update(id) => State_Panel.update(id)
+          case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
           case Protocol.Preview_Request(file, column) => request_preview(file, column)
           case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
           case _ => log("### IGNORED")

--- a/src/Tools/VSCode/src/state_panel.scala	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Thu Jun 29 11:36:25 2017 +0200
@@ -38,6 +38,10 @@
   def update(id: Counter.ID): Unit =
     instances.value.get(id).foreach(state =>
       state.server.editor.send_dispatcher(state.update()))
+
+  def auto_update(id: Counter.ID, enabled: Boolean): Unit =
+    instances.value.get(id).foreach(state =>
+      state.server.editor.send_dispatcher(state.auto_update(Some(enabled))))
 }
 
 
@@ -61,7 +65,8 @@
           val content =
             HTML.output_document(
               List(HTML.style(HTML.fonts_css()),
-                HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
+                HTML.style_file(Url.print_file(HTML.isabelle_css.file)),
+                HTML.script(controls_script)),
               List(controls, HTML.source(text)),
               css = "")
           output(content)
@@ -86,37 +91,52 @@
 
   private val auto_update_enabled = Synchronized(true)
 
-  def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
-
-  def auto_update() { if (auto_update_enabled.value) update() }
+  def auto_update(set: Option[Boolean] = None)
+  {
+    val enabled =
+      auto_update_enabled.guarded_access(a =>
+        set match {
+          case None => Some((a, a))
+          case Some(b) => Some((b, b))
+        })
+    if (enabled) update()
+  }
 
 
   /* controls */
 
-  private def id_parameter: XML.Elem =
-    HTML.GUI.parameter(id.toString, name = "id")
+  private def controls_script =
+    VSCode_JavaScript.invoke_command +
+"""
+function invoke_auto_update(enabled)
+{ invoke_command("_isabelle.state-auto-update", [""" + id + """, enabled]) }
+
+function invoke_update() { invoke_command("_isabelle.state-update", [""" + id + """]) }
+
+function invoke_locate() { invoke_command("_isabelle.state-locate", [""" + id + """]) }
+"""
 
   private def auto_update_button: XML.Elem =
     HTML.GUI.checkbox(HTML.text("Auto update"),
       name = "auto_update",
       tooltip = "Indicate automatic update following cursor movement",
-      submit = true,
-      selected = auto_update_enabled.value)
+      selected = auto_update_enabled.value,
+      script = "invoke_auto_update(this.checked)")
 
   private def update_button: XML.Elem =
     HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
       name = "update",
       tooltip = "Update display according to the command at cursor position",
-      submit = true)
+      script = "invoke_update()")
 
   private def locate_button: XML.Elem =
     HTML.GUI.button(HTML.text("Locate"),
       name = "locate",
       tooltip = "Locate printed command within source text",
-      submit = true)
+      script = "invoke_locate()")
 
   private val controls: XML.Elem =
-    HTML.Wrap_Panel(List(id_parameter, auto_update_button, update_button, locate_button))
+    HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button))
 
 
   /* main */

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/vscode_javascript.scala	Thu Jun 29 11:36:25 2017 +0200
@@ -0,0 +1,26 @@
+/*  Title:      Tools/VSCode/src/build_html.scala
+    Author:     Makarius
+
+JavaScript snipptes 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://")
+}
+"""
+}