HTML GUI actions via JavaScript;
authorwenzelm
Thu Jun 29 11:36:25 2017 +0200 (2017-06-29)
changeset 66211100c9c997e2b
parent 66210 a8b936749300
child 66212 f41396c15bb1
HTML GUI actions via JavaScript;
src/Pure/build-jars
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/protocol.ts
src/Tools/VSCode/extension/src/state_panel.ts
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
     1.1 --- a/src/Pure/build-jars	Wed Jun 28 14:17:05 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Thu Jun 29 11:36:25 2017 +0200
     1.3 @@ -172,6 +172,7 @@
     1.4    ../Tools/VSCode/src/protocol.scala
     1.5    ../Tools/VSCode/src/server.scala
     1.6    ../Tools/VSCode/src/state_panel.scala
     1.7 +  ../Tools/VSCode/src/vscode_javascript.scala
     1.8    ../Tools/VSCode/src/vscode_rendering.scala
     1.9    ../Tools/VSCode/src/vscode_resources.scala
    1.10    ../Tools/VSCode/src/vscode_spell_checker.scala
     2.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Wed Jun 28 14:17:05 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 11:36:25 2017 +0200
     2.3 @@ -107,7 +107,8 @@
     2.4      context.subscriptions.push(
     2.5        commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
     2.6        commands.registerCommand("_isabelle.state-locate", state_panel.locate),
     2.7 -      commands.registerCommand("_isabelle.state-update", state_panel.update))
     2.8 +      commands.registerCommand("_isabelle.state-update", state_panel.update),
     2.9 +      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update))
    2.10  
    2.11      language_client.onReady().then(() => state_panel.setup(context, language_client))
    2.12  
     3.1 --- a/src/Tools/VSCode/extension/src/protocol.ts	Wed Jun 28 14:17:05 2017 +0200
     3.2 +++ b/src/Tools/VSCode/extension/src/protocol.ts	Thu Jun 29 11:36:25 2017 +0200
     3.3 @@ -63,10 +63,18 @@
     3.4    id: number
     3.5  }
     3.6  
     3.7 +export interface Auto_Update
     3.8 +{
     3.9 +  id: number
    3.10 +  enabled: boolean
    3.11 +}
    3.12 +
    3.13  export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
    3.14  export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
    3.15  export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
    3.16  export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
    3.17 +export const state_auto_update_type =
    3.18 +  new NotificationType<Auto_Update, void>("PIDE/state_auto_update")
    3.19  
    3.20  
    3.21  /* preview */
     4.1 --- a/src/Tools/VSCode/extension/src/state_panel.ts	Wed Jun 28 14:17:05 2017 +0200
     4.2 +++ b/src/Tools/VSCode/extension/src/state_panel.ts	Thu Jun 29 11:36:25 2017 +0200
     4.3 @@ -76,3 +76,9 @@
     4.4  {
     4.5    if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
     4.6  }
     4.7 +
     4.8 +export function auto_update(id: number, enabled: boolean)
     4.9 +{
    4.10 +  if (language_client)
    4.11 +    language_client.sendNotification(protocol.state_auto_update_type, { id: id, enabled: enabled })
    4.12 +}
     5.1 --- a/src/Tools/VSCode/src/protocol.scala	Wed Jun 28 14:17:05 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 11:36:25 2017 +0200
     5.3 @@ -528,6 +528,19 @@
     5.4    object State_Locate extends State_Id_Notification("PIDE/state_locate")
     5.5    object State_Update extends State_Id_Notification("PIDE/state_update")
     5.6  
     5.7 +  object State_Auto_Update
     5.8 +  {
     5.9 +    def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] =
    5.10 +      json match {
    5.11 +        case Notification("PIDE/state_auto_update", Some(params)) =>
    5.12 +          for {
    5.13 +            id <- JSON.long(params, "id")
    5.14 +            enabled <- JSON.bool(params, "enabled")
    5.15 +          } yield (id, enabled)
    5.16 +        case _ => None
    5.17 +      }
    5.18 +  }
    5.19 +
    5.20  
    5.21    /* preview */
    5.22  
     6.1 --- a/src/Tools/VSCode/src/server.scala	Wed Jun 28 14:17:05 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Thu Jun 29 11:36:25 2017 +0200
     6.3 @@ -450,6 +450,7 @@
     6.4            case Protocol.State_Exit(id) => State_Panel.exit(id)
     6.5            case Protocol.State_Locate(id) => State_Panel.locate(id)
     6.6            case Protocol.State_Update(id) => State_Panel.update(id)
     6.7 +          case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
     6.8            case Protocol.Preview_Request(file, column) => request_preview(file, column)
     6.9            case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
    6.10            case _ => log("### IGNORED")
     7.1 --- a/src/Tools/VSCode/src/state_panel.scala	Wed Jun 28 14:17:05 2017 +0200
     7.2 +++ b/src/Tools/VSCode/src/state_panel.scala	Thu Jun 29 11:36:25 2017 +0200
     7.3 @@ -38,6 +38,10 @@
     7.4    def update(id: Counter.ID): Unit =
     7.5      instances.value.get(id).foreach(state =>
     7.6        state.server.editor.send_dispatcher(state.update()))
     7.7 +
     7.8 +  def auto_update(id: Counter.ID, enabled: Boolean): Unit =
     7.9 +    instances.value.get(id).foreach(state =>
    7.10 +      state.server.editor.send_dispatcher(state.auto_update(Some(enabled))))
    7.11  }
    7.12  
    7.13  
    7.14 @@ -61,7 +65,8 @@
    7.15            val content =
    7.16              HTML.output_document(
    7.17                List(HTML.style(HTML.fonts_css()),
    7.18 -                HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
    7.19 +                HTML.style_file(Url.print_file(HTML.isabelle_css.file)),
    7.20 +                HTML.script(controls_script)),
    7.21                List(controls, HTML.source(text)),
    7.22                css = "")
    7.23            output(content)
    7.24 @@ -86,37 +91,52 @@
    7.25  
    7.26    private val auto_update_enabled = Synchronized(true)
    7.27  
    7.28 -  def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
    7.29 -
    7.30 -  def auto_update() { if (auto_update_enabled.value) update() }
    7.31 +  def auto_update(set: Option[Boolean] = None)
    7.32 +  {
    7.33 +    val enabled =
    7.34 +      auto_update_enabled.guarded_access(a =>
    7.35 +        set match {
    7.36 +          case None => Some((a, a))
    7.37 +          case Some(b) => Some((b, b))
    7.38 +        })
    7.39 +    if (enabled) update()
    7.40 +  }
    7.41  
    7.42  
    7.43    /* controls */
    7.44  
    7.45 -  private def id_parameter: XML.Elem =
    7.46 -    HTML.GUI.parameter(id.toString, name = "id")
    7.47 +  private def controls_script =
    7.48 +    VSCode_JavaScript.invoke_command +
    7.49 +"""
    7.50 +function invoke_auto_update(enabled)
    7.51 +{ invoke_command("_isabelle.state-auto-update", [""" + id + """, enabled]) }
    7.52 +
    7.53 +function invoke_update() { invoke_command("_isabelle.state-update", [""" + id + """]) }
    7.54 +
    7.55 +function invoke_locate() { invoke_command("_isabelle.state-locate", [""" + id + """]) }
    7.56 +"""
    7.57  
    7.58    private def auto_update_button: XML.Elem =
    7.59      HTML.GUI.checkbox(HTML.text("Auto update"),
    7.60        name = "auto_update",
    7.61        tooltip = "Indicate automatic update following cursor movement",
    7.62 -      submit = true,
    7.63 -      selected = auto_update_enabled.value)
    7.64 +      selected = auto_update_enabled.value,
    7.65 +      script = "invoke_auto_update(this.checked)")
    7.66  
    7.67    private def update_button: XML.Elem =
    7.68      HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
    7.69        name = "update",
    7.70        tooltip = "Update display according to the command at cursor position",
    7.71 -      submit = true)
    7.72 +      script = "invoke_update()")
    7.73  
    7.74    private def locate_button: XML.Elem =
    7.75      HTML.GUI.button(HTML.text("Locate"),
    7.76        name = "locate",
    7.77        tooltip = "Locate printed command within source text",
    7.78 -      submit = true)
    7.79 +      script = "invoke_locate()")
    7.80  
    7.81    private val controls: XML.Elem =
    7.82 -    HTML.Wrap_Panel(List(id_parameter, auto_update_button, update_button, locate_button))
    7.83 +    HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button))
    7.84  
    7.85  
    7.86    /* main */
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/VSCode/src/vscode_javascript.scala	Thu Jun 29 11:36:25 2017 +0200
     8.3 @@ -0,0 +1,26 @@
     8.4 +/*  Title:      Tools/VSCode/src/build_html.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +JavaScript snipptes for VSCode HTML view.
     8.8 +*/
     8.9 +
    8.10 +package isabelle.vscode
    8.11 +
    8.12 +
    8.13 +import isabelle._
    8.14 +
    8.15 +
    8.16 +object VSCode_JavaScript
    8.17 +{
    8.18 +  val invoke_command =
    8.19 +"""
    8.20 +function invoke_command(name, args)
    8.21 +{
    8.22 +  window.parent.postMessage(
    8.23 +    {
    8.24 +      command: "did-click-link",
    8.25 +      data: "command:" + encodeURIComponent(name) + "?" + encodeURIComponent(JSON.stringify(args))
    8.26 +    }, "file://")
    8.27 +}
    8.28 +"""
    8.29 +}