src/Tools/VSCode/src/vscode_javascript.scala

HTML GUI actions via JavaScript;

/*  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://")
}
"""
}