# HG changeset patch
# User wenzelm
# Date 1319318951 -7200
# Node ID b769a3a370ad7ae471052237490b075db31efbe4
# Parent  3b7b64b194ee8cc3d1e0d0def27afe5b29075ab3
class Time as abstract datatype;

diff -r 3b7b64b194ee -r b769a3a370ad src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Sat Oct 22 23:28:24 2011 +0200
+++ b/src/Pure/General/timing.scala	Sat Oct 22 23:29:11 2011 +0200
@@ -12,7 +12,7 @@
   def ms(m: Long): Time = new Time(m)
 }
 
-class Time(val ms: Long)
+class Time private(val ms: Long)
 {
   def seconds: Double = ms / 1000.0
 
diff -r 3b7b64b194ee -r b769a3a370ad src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Oct 22 23:28:24 2011 +0200
+++ b/src/Pure/library.scala	Sat Oct 22 23:29:11 2011 +0200
@@ -219,7 +219,7 @@
     val stop = System.currentTimeMillis()
     System.err.println(
       (if (message == null || message.isEmpty) "" else message + ": ") +
-        new Time(stop - start).message + " elapsed time")
+        Time.ms(stop - start).message + " elapsed time")
     Exn.release(result)
   }
 }