1.1 --- a/src/Pure/General/timing.scala	Mon Nov 28 18:08:07 2011 +0100
     1.2 +++ b/src/Pure/General/timing.scala	Mon Nov 28 20:31:53 2011 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 +
     1.8  object Time
     1.9  {
    1.10    def seconds(s: Double): Time = new Time((s * 1000.0) round)
    1.11 @@ -24,6 +25,21 @@
    1.12    def message: String = toString + "s"
    1.13  }
    1.14  
    1.15 +
    1.16 +object Timing
    1.17 +{
    1.18 +  def timeit[A](message: String)(e: => A) =
    1.19 +  {
    1.20 +    val start = java.lang.System.currentTimeMillis()
    1.21 +    val result = Exn.capture(e)
    1.22 +    val stop = java.lang.System.currentTimeMillis()
    1.23 +    java.lang.System.err.println(
    1.24 +      (if (message == null || message.isEmpty) "" else message + ": ") +
    1.25 +        Time.ms(stop - start).message + " elapsed time")
    1.26 +    Exn.release(result)
    1.27 +  }
    1.28 +}
    1.29 +
    1.30  class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
    1.31  {
    1.32    def message: String =