1/* Title: Tools/VSCode/src/vscode_javascript.scala 2 Author: Makarius 3 4JavaScript snippets for VSCode HTML view. 5*/ 6 7package isabelle.vscode 8 9 10import isabelle._ 11 12 13object VSCode_JavaScript 14{ 15 val invoke_command = 16""" 17function 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} 27