# HG changeset patch # User wenzelm # Date 1646432559 -3600 # Node ID 1129e82dc1ec3a22a5eb38b676c48e8c90a12a14 # Parent a51a0a7048540b5fb9ce41042f1403a03a1dd3eb more robust; diff -r a51a0a704854 -r 1129e82dc1ec src/Tools/VSCode/src/vscode_setup.scala --- a/src/Tools/VSCode/src/vscode_setup.scala Fri Mar 04 22:53:49 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Fri Mar 04 23:22:39 2022 +0100 @@ -24,6 +24,9 @@ def vscode_workspace: Path = Path.variable("ISABELLE_VSCODE_WORKSPACE") def vscodium_home: Path = Path.variable("ISABELLE_VSCODIUM_HOME") + def vscodium_home_ok(): Boolean = + try { vscodium_home.is_dir } + catch { case ERROR(_) => false } def exe_path(dir: Path): Path = dir + Path.explode("bin/codium") @@ -141,7 +144,7 @@ } if (check) { - if (vscodium_home.is_dir) { + if (vscodium_home_ok()) { init_workspace(vscode_workspace) progress.echo(vscodium_home.expand.implode) }