src/Pure/General/timing.scala
author wenzelm
Sat, 14 Jan 2012 12:36:43 +0100
changeset 46204 df1369a42393
parent 45674 eb65c9d17e2f
child 46768 46acd255810d
permissions -rw-r--r--
tuned signature;
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
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    10
object Timing
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    11
{
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    12
  def timeit[A](message: String)(e: => A) =
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    13
  {
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    14
    val start = java.lang.System.currentTimeMillis()
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    15
    val result = Exn.capture(e)
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    16
    val stop = java.lang.System.currentTimeMillis()
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    17
    java.lang.System.err.println(
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    18
      (if (message == null || message.isEmpty) "" else message + ": ") +
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    19
        Time.ms(stop - start).message + " elapsed time")
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    20
    Exn.release(result)
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    21
  }
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    22
}
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    23
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    24
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
    25
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    26
  def message: String =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    27
    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
    28
  override def toString = message
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    29
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    30