src/Pure/General/timing.scala
author wenzelm
Sun Sep 04 15:49:59 2011 +0200 (2011-09-04)
changeset 44699 5199ee17c7d7
parent 40852 aee98c88c587
child 45249 b769a3a370ad
permissions -rw-r--r--
property "tooltip-dismiss-delay" is edited in ms, not seconds;
explicit tooltip_dismiss_delay boundaries for further robustness;
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@44699
    12
  def ms(m: Long): Time = new Time(m)
wenzelm@40393
    13
}
wenzelm@40393
    14
wenzelm@40848
    15
class Time(val ms: Long)
wenzelm@40848
    16
{
wenzelm@40848
    17
  def seconds: Double = ms / 1000.0
wenzelm@40852
    18
wenzelm@40852
    19
  def min(t: Time): Time = if (ms < t.ms) this else t
wenzelm@40852
    20
  def max(t: Time): Time = if (ms > t.ms) this else t
wenzelm@40852
    21
wenzelm@40848
    22
  override def toString =
wenzelm@40848
    23
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
wenzelm@40848
    24
  def message: String = toString + "s"
wenzelm@40848
    25
}
wenzelm@40848
    26
wenzelm@40848
    27
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
wenzelm@40848
    28
{
wenzelm@40848
    29
  def message: String =
wenzelm@40848
    30
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
wenzelm@40848
    31
  override def toString = message
wenzelm@40848
    32
}
wenzelm@40848
    33