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 =

     2.1 --- a/src/Pure/library.scala	Mon Nov 28 18:08:07 2011 +0100
     2.2 +++ b/src/Pure/library.scala	Mon Nov 28 20:31:53 2011 +0100
     2.3 @@ -208,20 +208,6 @@
     2.4      selection.index = 3
     2.5      prototypeDisplayValue = Some("00000%")
     2.6    }
     2.7 -
     2.8 -
     2.9 -  /* timing */
    2.10 -
    2.11 -  def timeit[A](message: String)(e: => A) =
    2.12 -  {
    2.13 -    val start = System.currentTimeMillis()
    2.14 -    val result = Exn.capture(e)
    2.15 -    val stop = System.currentTimeMillis()
    2.16 -    System.err.println(
    2.17 -      (if (message == null || message.isEmpty) "" else message + ": ") +
    2.18 -        Time.ms(stop - start).message + " elapsed time")
    2.19 -    Exn.release(result)
    2.20 -  }
    2.21  }
    2.22  
    2.23