more operations;
authorwenzelm
Fri Oct 07 16:50:47 2016 +0200 (2016-10-07)
changeset 64084bca58a11efde
parent 64083 fef1a0a59c12
child 64085 1c451e5c145f
more operations;
src/Pure/General/timing.scala
     1.1 --- a/src/Pure/General/timing.scala	Fri Oct 07 14:17:20 2016 +0200
     1.2 +++ b/src/Pure/General/timing.scala	Fri Oct 07 16:50:47 2016 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  /*  Title:      Pure/General/timing.scala
     1.5 -    Module:     PIDE
     1.6      Author:     Makarius
     1.7  
     1.8  Basic support for time measurement.
     1.9 @@ -36,25 +35,31 @@
    1.10  {
    1.11    def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
    1.12  
    1.13 +  def resources: Time = cpu + gc
    1.14 +
    1.15 +  def factor: Option[Double] =
    1.16 +  {
    1.17 +    val t1 = elapsed.seconds
    1.18 +    val t2 = resources.seconds
    1.19 +    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
    1.20 +  }
    1.21 +
    1.22    def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
    1.23  
    1.24    def message: String =
    1.25      elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
    1.26  
    1.27 -  def resources: Time = cpu + gc
    1.28    def message_resources: String =
    1.29    {
    1.30 -    val resources = cpu + gc
    1.31 -    val t1 = elapsed.seconds
    1.32 -    val t2 = resources.seconds
    1.33 -    val factor =
    1.34 -      if (t1 >= 3.0 && t2 >= 3.0)
    1.35 -        String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
    1.36 -      else ""
    1.37 -    if (t2 >= 3.0)
    1.38 -      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
    1.39 +    val factor_text =
    1.40 +      factor match {
    1.41 +        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
    1.42 +        case None => ""
    1.43 +      }
    1.44 +    if (resources.seconds >= 3.0)
    1.45 +      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
    1.46      else
    1.47 -      elapsed.message_hms + " elapsed time" + factor
    1.48 +      elapsed.message_hms + " elapsed time" + factor_text
    1.49    }
    1.50  
    1.51    override def toString: String = message