--- 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)) ++