src/Tools/VSCode/src/vscode_javascript.scala
author wenzelm
Mon, 25 Mar 2019 17:21:26 +0100
changeset 69981 3dced198b9ec
parent 66589 b884c42694e0
permissions -rw-r--r--
more strict AFP properties;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66589
b884c42694e0 tuned headers;
wenzelm
parents: 66219
diff changeset
     1
/*  Title:      Tools/VSCode/src/vscode_javascript.scala
66211
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     3
66219
f037cdaa5ca0 tuned spelling;
wenzelm
parents: 66211
diff changeset
     4
JavaScript snippets for VSCode HTML view.
66211
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     5
*/
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     6
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     7
package isabelle.vscode
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     8
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
     9
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    10
import isabelle._
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    11
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    12
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    13
object VSCode_JavaScript
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    14
{
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    15
  val invoke_command =
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    16
"""
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    17
function invoke_command(name, args)
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    18
{
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    19
  window.parent.postMessage(
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    20
    {
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    21
      command: "did-click-link",
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    22
      data: "command:" + encodeURIComponent(name) + "?" + encodeURIComponent(JSON.stringify(args))
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    23
    }, "file://")
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    24
}
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    25
"""
100c9c997e2b HTML GUI actions via JavaScript;
wenzelm
parents:
diff changeset
    26
}