src/Pure/Thy/sessions.scala
changeset 62633 e57416b649d5
parent 62632 cd991ba01ffd
child 62635 4854a38061de
--- a/src/Pure/Thy/sessions.scala	Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Mar 15 23:59:39 2016 +0100
@@ -335,16 +335,26 @@
       if (system_mode) Path.explode("~~/browser_info")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
-    private val input_dirs =
+    val input_dirs =
       if (system_mode) List(output_dir)
-      else output_dir :: Isabelle_System.find_logics_dirs()
+      else {
+        val ml_ident = Path.explode("$ML_IDENTIFIER").expand
+        output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
+      }
 
+    //optional heap + log_gz
     def find(name: String): Option[(Path, Path)] =
       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
         (dir + Path.basic(name), dir + log_gz(name)))
 
-    def find_log(name: String): Option[Path] = input_dirs.map(_ + log(name)).find(_.is_file)
-    def find_log_gz(name: String): Option[Path] = input_dirs.map(_ + log_gz(name)).find(_.is_file)
+    def find_heap(name: String): Option[Path] =
+      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
+
+    def find_log(name: String): Option[Path] =
+      input_dirs.map(_ + log(name)).find(_.is_file)
+
+    def find_log_gz(name: String): Option[Path] =
+      input_dirs.map(_ + log_gz(name)).find(_.is_file)
 
     def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
   }