enable vscode_unicode_symbols by default, despite asymmetry of input and output;
authorwenzelm
Wed, 11 Jan 2017 16:25:15 +0100
changeset 64874 e13ff666af96
parent 64873 ee5aaf7bce0d
child 64875 4efffde18a90
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Jan 11 16:11:39 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Jan 11 16:25:15 2017 +0100
@@ -22,12 +22,13 @@
     vscode.window.showErrorMessage("Missing user settings: isabelle.home")
   else {
     let isabelle_tool = isabelle_home.concat("/bin/isabelle")
+    let standard_args = ["-o", "vscode_unicode_symbols"]
     let run =
       is_windows ?
         { command: cygwin_root.concat("/bin/bash"),
-          args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } :
+          args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
         { command: isabelle_tool,
-          args: ["vscode_server"].concat(isabelle_args) };
+          args: ["vscode_server"].concat(standard_args, isabelle_args) };
 
     let server_options: ServerOptions = { run: run, debug: run };
     let client_options: LanguageClientOptions = {