# HG changeset patch # User wenzelm # Date 1484148315 -3600 # Node ID e13ff666af96163e4e1a6193119b217bb964fdb2 # Parent ee5aaf7bce0db4742a73b8780084fd9f7dd12990 enable vscode_unicode_symbols by default, despite asymmetry of input and output; diff -r ee5aaf7bce0d -r e13ff666af96 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 = {