early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
authorwenzelm
Wed, 12 Apr 2017 17:48:19 +0200
changeset 65468 c41791ad75c3
parent 65467 9535c670b1b4
child 65469 78ace4a14975
early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
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)
   }