src/Pure/General/time.scala
changeset 61528 053f7083b3eb
parent 57912 dd9550f84106
child 61602 a2f0f659a3c2
--- a/src/Pure/General/time.scala	Fri Oct 30 17:14:30 2015 +0100
+++ b/src/Pure/General/time.scala	Sat Oct 31 14:16:29 2015 +0100
@@ -15,8 +15,10 @@
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
+  def now(): Time = ms(System.currentTimeMillis())
+
   val zero: Time = ms(0)
-  def now(): Time = ms(System.currentTimeMillis())
+  val start: Time = now()
 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])