src/Pure/General/timing.scala
author wenzelm
Thu Apr 24 11:01:14 2014 +0200 (2014-04-24)
changeset 56691 ad5d7461b370
parent 55618 995162143ef4
child 56782 433cf57550fa
permissions -rw-r--r--
tuned signature, in accordance to ML version;
wenzelm@40393
     1
/*  Title:      Pure/General/timing.scala
wenzelm@46768
     2
    Module:     PIDE
wenzelm@40393
     3
    Author:     Makarius
wenzelm@40393
     4
wenzelm@40393
     5
Basic support for time measurement.
wenzelm@40393
     6
*/
wenzelm@40393
     7
wenzelm@40393
     8
package isabelle
wenzelm@40393
     9
wenzelm@45664
    10
wenzelm@45664
    11
object Timing
wenzelm@45664
    12
{
wenzelm@51587
    13
  val zero = Timing(Time.zero, Time.zero, Time.zero)
wenzelm@51587
    14
wenzelm@47653
    15
  def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
wenzelm@47653
    16
    if (enabled) {
wenzelm@56691
    17
      val start = Time.now()
wenzelm@47653
    18
      val result = Exn.capture(e)
wenzelm@56691
    19
      val stop = Time.now()
wenzelm@46768
    20
wenzelm@56691
    21
      val timing = stop - start
wenzelm@47653
    22
      if (timing.is_relevant)
wenzelm@55618
    23
        System.err.println(
wenzelm@47653
    24
          (if (message == null || message.isEmpty) "" else message + ": ") +
wenzelm@47653
    25
            timing.message + " elapsed time")
wenzelm@46768
    26
wenzelm@47653
    27
      Exn.release(result)
wenzelm@47653
    28
    }
wenzelm@47653
    29
    else e
wenzelm@45664
    30
}
wenzelm@45664
    31
wenzelm@51587
    32
sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
wenzelm@40848
    33
{
wenzelm@46768
    34
  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
wenzelm@46768
    35
wenzelm@51587
    36
  def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
wenzelm@51587
    37
wenzelm@40848
    38
  def message: String =
wenzelm@40848
    39
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
wenzelm@46768
    40
wenzelm@40848
    41
  override def toString = message
wenzelm@40848
    42
}
wenzelm@40848
    43