src/Pure/Tools/build_log.scala
changeset 64089 10d719dbb3ee
parent 64088 210aabe359ab
child 64090 5a68280112b3
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:07:10 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
     1.3 @@ -243,8 +243,8 @@
     1.4      chapter: String,
     1.5      groups: List[String],
     1.6      threads: Option[Int],
     1.7 -    timing: Option[Timing],
     1.8 -    ml_timing: Option[Timing],
     1.9 +    timing: Timing,
    1.10 +    ml_timing: Timing,
    1.11      status: Session_Status.Value)
    1.12    {
    1.13      def finished: Boolean = status == Session_Status.FINISHED
    1.14 @@ -255,17 +255,15 @@
    1.15      def session(name: String): Session_Entry = sessions(name)
    1.16      def get_session(name: String): Option[Session_Entry] = sessions.get(name)
    1.17  
    1.18 -    def finished(name: String): Boolean =
    1.19 +    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
    1.20        get_session(name) match {
    1.21 -        case Some(entry) => entry.finished
    1.22 -        case None => false
    1.23 +        case Some(entry) => f(entry)
    1.24 +        case None => x
    1.25        }
    1.26  
    1.27 -    def timing(name: String): Timing =
    1.28 -      (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero
    1.29 -
    1.30 -    def ml_timing(name: String): Timing =
    1.31 -      (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero
    1.32 +    def finished(name: String): Boolean = get_default(name, _.finished, false)
    1.33 +    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
    1.34 +    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
    1.35    }
    1.36  
    1.37    private def parse_build_info(log_file: Log_File): Build_Info =
    1.38 @@ -350,8 +348,8 @@
    1.39                chapter.getOrElse(name, ""),
    1.40                groups.getOrElse(name, Nil),
    1.41                threads.get(name),
    1.42 -              timing.get(name),
    1.43 -              ml_timing.get(name),
    1.44 +              timing.getOrElse(name, Timing.zero),
    1.45 +              ml_timing.getOrElse(name, Timing.zero),
    1.46                status)
    1.47            (name -> entry)
    1.48          }):_*)