# HG changeset patch
# User wenzelm
# Date 1647971788 -3600
# Node ID fc4d075876955fd5a5c492f1e23789c6365e2b90
# Parent  d92e0197ba01e84624ac899240d85509b8c777d1
more robust errors -- on foreground process instead of background server;

diff -r d92e0197ba01 -r fc4d07587695 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Mar 22 18:52:27 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Mar 22 18:56:28 2022 +0100
@@ -1013,7 +1013,7 @@
   def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
-  private def check_session_dir(dir: Path): Path =
+  def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString)
 
diff -r d92e0197ba01 -r fc4d07587695 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Tue Mar 22 18:52:27 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Tue Mar 22 18:56:28 2022 +0100
@@ -36,7 +36,8 @@
       JSON.optional("logic" -> proper_string(logic)) ++
       JSON.optional("logic_ancestor" -> proper_string(logic_ancestor)) ++
       JSON.optional("logic_requirements" -> proper_bool(logic_requirements)) ++
-      JSON.optional("session_dirs" -> proper_list(session_dirs.map(_.absolute.implode))) ++
+      JSON.optional("session_dirs" ->
+        proper_list(session_dirs.map(dir => Sessions.check_session_dir(dir).absolute.implode))) ++
       JSON.optional("include_sessions" -> proper_list(include_sessions)) ++
       JSON.optional("modes" -> proper_list(modes)) ++
       JSON.optional("no_build" -> proper_bool(no_build)) ++