src/Pure/General/timing.scala
author wenzelm
Mon Nov 28 20:31:53 2011 +0100 (2011-11-28)
changeset 45664 ac6e704dcd12
parent 45249 b769a3a370ad
child 45667 546d78f0d81f
permissions -rw-r--r--
tuned signature (according to ML version);
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@45664
     9
wenzelm@40848
    10
object Time
wenzelm@40393
    11
{
wenzelm@40848
    12
  def seconds(s: Double): Time = new Time((s * 1000.0) round)
wenzelm@44699
    13
  def ms(m: Long): Time = new Time(m)
wenzelm@40393
    14
}
wenzelm@40393
    15
wenzelm@45249
    16
class Time private(val ms: Long)
wenzelm@40848
    17
{
wenzelm@40848
    18
  def seconds: Double = ms / 1000.0
wenzelm@40852
    19
wenzelm@40852
    20
  def min(t: Time): Time = if (ms < t.ms) this else t
wenzelm@40852
    21
  def max(t: Time): Time = if (ms > t.ms) this else t
wenzelm@40852
    22
wenzelm@40848
    23
  override def toString =
wenzelm@40848
    24
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
wenzelm@40848
    25
  def message: String = toString + "s"
wenzelm@40848
    26
}
wenzelm@40848
    27
wenzelm@45664
    28
wenzelm@45664
    29
object Timing
wenzelm@45664
    30
{
wenzelm@45664
    31
  def timeit[A](message: String)(e: => A) =
wenzelm@45664
    32
  {
wenzelm@45664
    33
    val start = java.lang.System.currentTimeMillis()
wenzelm@45664
    34
    val result = Exn.capture(e)
wenzelm@45664
    35
    val stop = java.lang.System.currentTimeMillis()
wenzelm@45664
    36
    java.lang.System.err.println(
wenzelm@45664
    37
      (if (message == null || message.isEmpty) "" else message + ": ") +
wenzelm@45664
    38
        Time.ms(stop - start).message + " elapsed time")
wenzelm@45664
    39
    Exn.release(result)
wenzelm@45664
    40
  }
wenzelm@45664
    41
}
wenzelm@45664
    42
wenzelm@40848
    43
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
wenzelm@40848
    44
{
wenzelm@40848
    45
  def message: String =
wenzelm@40848
    46
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
wenzelm@40848
    47
  override def toString = message
wenzelm@40848
    48
}
wenzelm@40848
    49