author | wenzelm |
Thu, 29 Jun 2017 20:59:49 +0200 | |
changeset 66219 | f037cdaa5ca0 |
parent 66211 | 100c9c997e2b |
child 66589 | b884c42694e0 |
permissions | -rw-r--r-- |
/* Title: Tools/VSCode/src/build_html.scala Author: Makarius JavaScript snippets 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://") } """ }