--- a/src/Tools/VSCode/extension/src/extension.ts Sun Jan 01 13:15:50 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Sun Jan 01 13:38:20 2017 +0100
@@ -9,11 +9,13 @@
export function activate(context: vscode.ExtensionContext)
{
- let isabelle_home = vscode.workspace.getConfiguration("isabelle").get("home");
+ let isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
+ let isabelle_arguments =
+ vscode.workspace.getConfiguration("isabelle").get<Array<string>>("arguments");
let run = {
command: path.join(isabelle_home, "bin", "isabelle"),
- args: ["vscode_server"]
+ args: ["vscode_server"].concat(isabelle_arguments)
};
let server_options: ServerOptions =
{