1.1 --- a/src/Pure/Tools/build.scala	Tue Feb 19 16:49:40 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Feb 19 17:02:52 2013 +0100
     1.3 @@ -656,27 +656,34 @@
     1.4           Path.explode("$ISABELLE_BROWSER_INFO"))
     1.5        }
     1.6  
     1.7 -    def find_log(name: String): Option[Path] =
     1.8 -      input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir => dir + log_gz(name))
     1.9 +    def find_log(name: String): Option[(Path, Path)] =
    1.10 +      input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
    1.11  
    1.12  
    1.13      /* queue with scheduling information */
    1.14  
    1.15      def get_timing(name: String): (List[Properties.T], Double) =
    1.16 -      find_log(name) match {
    1.17 -        case Some(path) =>
    1.18 -          try {
    1.19 -            val info = parse_log(false, File.read_gzip(path))
    1.20 -            val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.21 -            (info.command_timings, session_timing)
    1.22 -          }
    1.23 -          catch {
    1.24 -            case ERROR(msg) =>
    1.25 -              java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
    1.26 -            (Nil, 0.0)
    1.27 -          }
    1.28 -        case None => (Nil, 0.0)
    1.29 +    {
    1.30 +      val (path, text) =
    1.31 +        find_log(name + ".gz") match {
    1.32 +          case Some((_, path)) => (path, File.read_gzip(path))
    1.33 +          case None =>
    1.34 +            find_log(name) match {
    1.35 +              case Some((_, path)) => (path, File.read(path))
    1.36 +              case None => (Path.current, "")
    1.37 +            }
    1.38 +        }
    1.39 +      try {
    1.40 +        val info = parse_log(false, text)
    1.41 +        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.42 +        (info.command_timings, session_timing)
    1.43        }
    1.44 +      catch {
    1.45 +        case ERROR(msg) =>
    1.46 +          java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
    1.47 +        (Nil, 0.0)
    1.48 +      }
    1.49 +    }
    1.50  
    1.51      val queue = Queue(selected_tree, get_timing)
    1.52  
    1.53 @@ -768,11 +775,11 @@
    1.54  
    1.55                  val (current, heap) =
    1.56                  {
    1.57 -                  find_log(name) match {
    1.58 -                    case Some(path) =>
    1.59 +                  find_log(name + ".gz") match {
    1.60 +                    case Some((dir, path)) =>
    1.61                        read_stamps(path) match {
    1.62                          case Some((s, h1, h2)) =>
    1.63 -                          val heap = heap_stamp(Some(path.dir + Path.basic(name)))
    1.64 +                          val heap = heap_stamp(Some(dir + Path.basic(name)))
    1.65                            (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
    1.66                              !(do_output && heap == no_heap), heap)
    1.67                          case None => (false, no_heap)