# 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)
       }