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