# HG changeset patch
# User wenzelm
# Date 1361289772 -3600
# Node ID e8ac22bb2b28da803b29e020d7dfc16cbe4b0edf
# Parent  e140c8fa485ad5783049b4b3c88324669c281993
read logs from failed sessions as well;
proper output base directory (which is two steps upwards);

diff -r e140c8fa485a -r e8ac22bb2b28 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Feb 19 16:49:40 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Feb 19 17:02:52 2013 +0100
@@ -656,27 +656,34 @@
          Path.explode("$ISABELLE_BROWSER_INFO"))
       }
 
-    def find_log(name: String): Option[Path] =
-      input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir => dir + log_gz(name))
+    def find_log(name: String): Option[(Path, Path)] =
+      input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
 
 
     /* queue with scheduling information */
 
     def get_timing(name: String): (List[Properties.T], Double) =
-      find_log(name) match {
-        case Some(path) =>
-          try {
-            val info = parse_log(false, File.read_gzip(path))
-            val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
-            (info.command_timings, session_timing)
-          }
-          catch {
-            case ERROR(msg) =>
-              java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
-            (Nil, 0.0)
-          }
-        case None => (Nil, 0.0)
+    {
+      val (path, text) =
+        find_log(name + ".gz") match {
+          case Some((_, path)) => (path, File.read_gzip(path))
+          case None =>
+            find_log(name) match {
+              case Some((_, path)) => (path, File.read(path))
+              case None => (Path.current, "")
+            }
+        }
+      try {
+        val info = parse_log(false, text)
+        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
+        (info.command_timings, session_timing)
       }
+      catch {
+        case ERROR(msg) =>
+          java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
+        (Nil, 0.0)
+      }
+    }
 
     val queue = Queue(selected_tree, get_timing)
 
@@ -768,11 +775,11 @@
 
                 val (current, heap) =
                 {
-                  find_log(name) match {
-                    case Some(path) =>
+                  find_log(name + ".gz") match {
+                    case Some((dir, path)) =>
                       read_stamps(path) match {
                         case Some((s, h1, h2)) =>
-                          val heap = heap_stamp(Some(path.dir + Path.basic(name)))
+                          val heap = heap_stamp(Some(dir + Path.basic(name)))
                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
                             !(do_output && heap == no_heap), heap)
                         case None => (false, no_heap)