# HG changeset patch # User wenzelm # Date 1498728985 -7200 # Node ID 100c9c997e2b3bc87bbe152847271675e07ead1d # Parent a8b93674930041470ff74c4da41195b742973ff6 HTML GUI actions via JavaScript; diff -r a8b936749300 -r 100c9c997e2b src/Pure/build-jars --- 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 diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/extension/src/extension.ts --- 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)) diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/extension/src/protocol.ts --- 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("PIDE/state_init") export const state_exit_type = new NotificationType("PIDE/state_exit") export const state_locate_type = new NotificationType("PIDE/state_locate") export const state_update_type = new NotificationType("PIDE/state_update") +export const state_auto_update_type = + new NotificationType("PIDE/state_auto_update") /* preview */ diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/extension/src/state_panel.ts --- 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 }) +} diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/src/protocol.scala --- 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 */ diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/src/server.scala --- 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") diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/src/state_panel.scala --- 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 */ diff -r a8b936749300 -r 100c9c997e2b src/Tools/VSCode/src/vscode_javascript.scala --- /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://") +} +""" +}