more robust errors -- on foreground process instead of background server;
authorwenzelm
Tue, 22 Mar 2022 18:56:28 +0100
changeset 75297 fc4d07587695
parent 75296 d92e0197ba01
child 75298 064e44da2e88
more robust errors -- on foreground process instead of background server;
src/Pure/Thy/sessions.scala
src/Tools/VSCode/src/vscode_main.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)
 
--- 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)) ++