more permissive timing data;
authorwenzelm
Fri Oct 07 18:30:56 2016 +0200 (2016-10-07)
changeset 6408910d719dbb3ee
parent 64088 210aabe359ab
child 64090 5a68280112b3
more permissive timing data;
src/Pure/General/timing.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/build_stats.scala
     1.1 --- a/src/Pure/General/timing.scala	Fri Oct 07 18:07:10 2016 +0200
     1.2 +++ b/src/Pure/General/timing.scala	Fri Oct 07 18:30:56 2016 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4  
     1.5  sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
     1.6  {
     1.7 +  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
     1.8    def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
     1.9  
    1.10    def resources: Time = cpu + gc
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:07:10 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
     2.3 @@ -243,8 +243,8 @@
     2.4      chapter: String,
     2.5      groups: List[String],
     2.6      threads: Option[Int],
     2.7 -    timing: Option[Timing],
     2.8 -    ml_timing: Option[Timing],
     2.9 +    timing: Timing,
    2.10 +    ml_timing: Timing,
    2.11      status: Session_Status.Value)
    2.12    {
    2.13      def finished: Boolean = status == Session_Status.FINISHED
    2.14 @@ -255,17 +255,15 @@
    2.15      def session(name: String): Session_Entry = sessions(name)
    2.16      def get_session(name: String): Option[Session_Entry] = sessions.get(name)
    2.17  
    2.18 -    def finished(name: String): Boolean =
    2.19 +    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
    2.20        get_session(name) match {
    2.21 -        case Some(entry) => entry.finished
    2.22 -        case None => false
    2.23 +        case Some(entry) => f(entry)
    2.24 +        case None => x
    2.25        }
    2.26  
    2.27 -    def timing(name: String): Timing =
    2.28 -      (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero
    2.29 -
    2.30 -    def ml_timing(name: String): Timing =
    2.31 -      (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero
    2.32 +    def finished(name: String): Boolean = get_default(name, _.finished, false)
    2.33 +    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
    2.34 +    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
    2.35    }
    2.36  
    2.37    private def parse_build_info(log_file: Log_File): Build_Info =
    2.38 @@ -350,8 +348,8 @@
    2.39                chapter.getOrElse(name, ""),
    2.40                groups.getOrElse(name, Nil),
    2.41                threads.get(name),
    2.42 -              timing.get(name),
    2.43 -              ml_timing.get(name),
    2.44 +              timing.getOrElse(name, Timing.zero),
    2.45 +              ml_timing.getOrElse(name, Timing.zero),
    2.46                status)
    2.47            (name -> entry)
    2.48          }):_*)
     3.1 --- a/src/Pure/Tools/build_stats.scala	Fri Oct 07 18:07:10 2016 +0200
     3.2 +++ b/src/Pure/Tools/build_stats.scala	Fri Oct 07 18:30:56 2016 +0200
     3.3 @@ -35,8 +35,10 @@
     3.4          { case (s, (_, info)) => s ++ info.sessions.keySet })
     3.5  
     3.6      def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
     3.7 -      (for (entry <- info.get_session(session); t <- entry.timing)
     3.8 -        yield t.elapsed >= elapsed_threshold) getOrElse false
     3.9 +    {
    3.10 +      val t = info.timing(session)
    3.11 +      !t.is_zero && t.elapsed >= elapsed_threshold
    3.12 +    }
    3.13  
    3.14      val sessions =
    3.15        for {