src/Pure/General/timing.scala
author wenzelm
Mon, 28 Nov 2011 20:31:53 +0100
changeset 45664 ac6e704dcd12
parent 45249 b769a3a370ad
child 45667 546d78f0d81f
permissions -rw-r--r--
tuned signature (according to ML version);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/timing.scala
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     3
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     4
Basic support for time measurement.
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     5
*/
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     6
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     8
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
     9
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    10
object Time
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    11
{
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    12
  def seconds(s: Double): Time = new Time((s * 1000.0) round)
44699
5199ee17c7d7 property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents: 40852
diff changeset
    13
  def ms(m: Long): Time = new Time(m)
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    14
}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    15
45249
b769a3a370ad class Time as abstract datatype;
wenzelm
parents: 44699
diff changeset
    16
class Time private(val ms: Long)
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    17
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    18
  def seconds: Double = ms / 1000.0
40852
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    19
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    20
  def min(t: Time): Time = if (ms < t.ms) this else t
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    21
  def max(t: Time): Time = if (ms > t.ms) this else t
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    22
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    23
  override def toString =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    24
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    25
  def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    26
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    27
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    28
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    29
object Timing
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    30
{
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    31
  def timeit[A](message: String)(e: => A) =
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    32
  {
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    33
    val start = java.lang.System.currentTimeMillis()
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    34
    val result = Exn.capture(e)
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    35
    val stop = java.lang.System.currentTimeMillis()
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    36
    java.lang.System.err.println(
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    37
      (if (message == null || message.isEmpty) "" else message + ": ") +
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    38
        Time.ms(stop - start).message + " elapsed time")
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    39
    Exn.release(result)
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    40
  }
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    41
}
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    42
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    43
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    44
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    45
  def message: String =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    46
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    47
  override def toString = message
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    48
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    49