66589
|
1 |
/* Title: Tools/VSCode/src/vscode_javascript.scala
|
66211
|
2 |
Author: Makarius
|
|
3 |
|
66219
|
4 |
JavaScript snippets for VSCode HTML view.
|
66211
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.vscode
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
|
|
13 |
object VSCode_JavaScript
|
|
14 |
{
|
|
15 |
val invoke_command =
|
|
16 |
"""
|
|
17 |
function invoke_command(name, args)
|
|
18 |
{
|
|
19 |
window.parent.postMessage(
|
|
20 |
{
|
|
21 |
command: "did-click-link",
|
|
22 |
data: "command:" + encodeURIComponent(name) + "?" + encodeURIComponent(JSON.stringify(args))
|
|
23 |
}, "file://")
|
|
24 |
}
|
|
25 |
"""
|
|
26 |
}
|