# HG changeset patch
# User wenzelm
# Date 1322508713 -3600
# Node ID ac6e704dcd12fa618dd1bc2efd520a9d2dce1a22
# Parent  d32ec2234efc66da7aec1a58b623a11eab61c36c
tuned signature (according to ML version);

diff -r d32ec2234efc -r ac6e704dcd12 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Mon Nov 28 18:08:07 2011 +0100
+++ b/src/Pure/General/timing.scala	Mon Nov 28 20:31:53 2011 +0100
@@ -6,6 +6,7 @@
 
 package isabelle
 
+
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0) round)
@@ -24,6 +25,21 @@
   def message: String = toString + "s"
 }
 
+
+object Timing
+{
+  def timeit[A](message: String)(e: => A) =
+  {
+    val start = java.lang.System.currentTimeMillis()
+    val result = Exn.capture(e)
+    val stop = java.lang.System.currentTimeMillis()
+    java.lang.System.err.println(
+      (if (message == null || message.isEmpty) "" else message + ": ") +
+        Time.ms(stop - start).message + " elapsed time")
+    Exn.release(result)
+  }
+}
+
 class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
 {
   def message: String =
diff -r d32ec2234efc -r ac6e704dcd12 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Nov 28 18:08:07 2011 +0100
+++ b/src/Pure/library.scala	Mon Nov 28 20:31:53 2011 +0100
@@ -208,20 +208,6 @@
     selection.index = 3
     prototypeDisplayValue = Some("00000%")
   }
-
-
-  /* timing */
-
-  def timeit[A](message: String)(e: => A) =
-  {
-    val start = System.currentTimeMillis()
-    val result = Exn.capture(e)
-    val stop = System.currentTimeMillis()
-    System.err.println(
-      (if (message == null || message.isEmpty) "" else message + ": ") +
-        Time.ms(stop - start).message + " elapsed time")
-    Exn.release(result)
-  }
 }