# HG changeset patch
# User wenzelm
# Date 1475857856 -7200
# Node ID 10d719dbb3ee4d45fa6da254572ac63891628b4c
# Parent  210aabe359ab9c4ccdfda4403d5e8a36771b1955
more permissive timing data;

diff -r 210aabe359ab -r 10d719dbb3ee src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Fri Oct 07 18:07:10 2016 +0200
+++ b/src/Pure/General/timing.scala	Fri Oct 07 18:30:56 2016 +0200
@@ -33,6 +33,7 @@
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
 {
+  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
   def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
 
   def resources: Time = cpu + gc
diff -r 210aabe359ab -r 10d719dbb3ee src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:07:10 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
@@ -243,8 +243,8 @@
     chapter: String,
     groups: List[String],
     threads: Option[Int],
-    timing: Option[Timing],
-    ml_timing: Option[Timing],
+    timing: Timing,
+    ml_timing: Timing,
     status: Session_Status.Value)
   {
     def finished: Boolean = status == Session_Status.FINISHED
@@ -255,17 +255,15 @@
     def session(name: String): Session_Entry = sessions(name)
     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
 
-    def finished(name: String): Boolean =
+    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
       get_session(name) match {
-        case Some(entry) => entry.finished
-        case None => false
+        case Some(entry) => f(entry)
+        case None => x
       }
 
-    def timing(name: String): Timing =
-      (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero
-
-    def ml_timing(name: String): Timing =
-      (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero
+    def finished(name: String): Boolean = get_default(name, _.finished, false)
+    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
+    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   }
 
   private def parse_build_info(log_file: Log_File): Build_Info =
@@ -350,8 +348,8 @@
               chapter.getOrElse(name, ""),
               groups.getOrElse(name, Nil),
               threads.get(name),
-              timing.get(name),
-              ml_timing.get(name),
+              timing.getOrElse(name, Timing.zero),
+              ml_timing.getOrElse(name, Timing.zero),
               status)
           (name -> entry)
         }):_*)
diff -r 210aabe359ab -r 10d719dbb3ee src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Fri Oct 07 18:07:10 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Fri Oct 07 18:30:56 2016 +0200
@@ -35,8 +35,10 @@
         { case (s, (_, info)) => s ++ info.sessions.keySet })
 
     def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
-      (for (entry <- info.get_session(session); t <- entry.timing)
-        yield t.elapsed >= elapsed_threshold) getOrElse false
+    {
+      val t = info.timing(session)
+      !t.is_zero && t.elapsed >= elapsed_threshold
+    }
 
     val sessions =
       for {