# HG changeset patch
# User wenzelm
# Date 1492012099 -7200
# Node ID c41791ad75c39b61c95a08927fcba04539e2ce7b
# Parent  9535c670b1b417544fe365da755c6e211369c6d5
early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;

diff -r 9535c670b1b4 -r c41791ad75c3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Apr 12 14:59:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 12 17:48:19 2017 +0200
@@ -595,7 +595,7 @@
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   private def check_session_dir(dir: Path): Path =
-    if (is_session_dir(dir)) dir
+    if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory: " + dir.toString)
 
   def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
@@ -626,13 +626,11 @@
     }
 
     val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
-    dirs.foreach(check_session_dir(_))
-    select_dirs.foreach(check_session_dir(_))
 
     make(
       for {
         (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
-        info <- load_dir(select, dir)
+        info <- load_dir(select, check_session_dir(dir))
       } yield info)
   }