src/Pure/General/timing.scala
author wenzelm
Wed Dec 01 20:34:40 2010 +0100 (2010-12-01)
changeset 40848 8662b9b1f123
parent 40393 2bb7ec08574a
child 40852 aee98c88c587
permissions -rw-r--r--
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm@40393
     1
/*  Title:      Pure/General/timing.scala
wenzelm@40393
     2
    Author:     Makarius
wenzelm@40393
     3
wenzelm@40393
     4
Basic support for time measurement.
wenzelm@40393
     5
*/
wenzelm@40393
     6
wenzelm@40393
     7
package isabelle
wenzelm@40393
     8
wenzelm@40848
     9
object Time
wenzelm@40393
    10
{
wenzelm@40848
    11
  def seconds(s: Double): Time = new Time((s * 1000.0) round)
wenzelm@40393
    12
}
wenzelm@40393
    13
wenzelm@40848
    14
class Time(val ms: Long)
wenzelm@40848
    15
{
wenzelm@40848
    16
  def seconds: Double = ms / 1000.0
wenzelm@40848
    17
  override def toString =
wenzelm@40848
    18
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
wenzelm@40848
    19
  def message: String = toString + "s"
wenzelm@40848
    20
}
wenzelm@40848
    21
wenzelm@40848
    22
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
wenzelm@40848
    23
{
wenzelm@40848
    24
  def message: String =
wenzelm@40848
    25
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
wenzelm@40848
    26
  override def toString = message
wenzelm@40848
    27
}
wenzelm@40848
    28