src/Pure/General/timing.scala
author wenzelm
Thu Dec 02 10:46:03 2010 +0100 (2010-12-02)
changeset 40852 aee98c88c587
parent 40848 8662b9b1f123
child 44699 5199ee17c7d7
permissions -rw-r--r--
builtin time bounds (again);
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@40852
    17
wenzelm@40852
    18
  def min(t: Time): Time = if (ms < t.ms) this else t
wenzelm@40852
    19
  def max(t: Time): Time = if (ms > t.ms) this else t
wenzelm@40852
    20
wenzelm@40848
    21
  override def toString =
wenzelm@40848
    22
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
wenzelm@40848
    23
  def message: String = toString + "s"
wenzelm@40848
    24
}
wenzelm@40848
    25
wenzelm@40848
    26
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
wenzelm@40848
    27
{
wenzelm@40848
    28
  def message: String =
wenzelm@40848
    29
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
wenzelm@40848
    30
  override def toString = message
wenzelm@40848
    31
}
wenzelm@40848
    32