diff -r 5f946e8887c5 -r ebaf9d01a964 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Mon Jan 02 09:38:06 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Mon Jan 02 09:39:00 2017 +0100 @@ -10,12 +10,11 @@ export function activate(context: vscode.ExtensionContext) { let isabelle_home = vscode.workspace.getConfiguration("isabelle").get("home"); - let isabelle_arguments = - vscode.workspace.getConfiguration("isabelle").get>("arguments"); + let isabelle_args = vscode.workspace.getConfiguration("isabelle").get>("args"); let run = { command: path.join(isabelle_home, "bin", "isabelle"), - args: ["vscode_server"].concat(isabelle_arguments) + args: ["vscode_server"].concat(isabelle_args) }; let server_options: ServerOptions = {