author | wenzelm |
Sat, 01 Jun 2019 11:29:59 +0200 | |
changeset 70299 | 83774d669b51 |
parent 66589 | b884c42694e0 |
permissions | -rw-r--r-- |
/* Title: Tools/VSCode/src/vscode_javascript.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://") } """ }