global start time as reference point;
authorwenzelm
Sat, 31 Oct 2015 14:16:29 +0100
changeset 61528 053f7083b3eb
parent 61527 d05f3d86a758
child 61529 82fc5a6231a2
global start time as reference point;
src/Pure/General/time.scala
--- 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])