author | wenzelm |
Thu, 29 Jun 2017 11:36:25 +0200 | |
changeset 66211 | 100c9c997e2b |
child 66219 | f037cdaa5ca0 |
permissions | -rw-r--r-- |
66211 | 1 |
/* Title: Tools/VSCode/src/build_html.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
JavaScript snipptes for VSCode HTML view. |
|
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 |
} |