--- a/src/Pure/General/timing.scala Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/General/timing.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,4 @@
/* Title: Pure/General/timing.scala
- Module: PIDE
Author: Makarius
Basic support for time measurement.
@@ -8,25 +7,6 @@
package isabelle
-object Time
-{
- def seconds(s: Double): Time = new Time((s * 1000.0) round)
- def ms(m: Long): Time = new Time(m)
-}
-
-class Time private(val ms: Long)
-{
- def seconds: Double = ms / 1000.0
-
- def min(t: Time): Time = if (ms < t.ms) this else t
- def max(t: Time): Time = if (ms > t.ms) this else t
-
- override def toString =
- String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
- def message: String = toString + "s"
-}
-
-
object Timing
{
def timeit[A](message: String)(e: => A) =