# HG changeset patch
# User wenzelm
# Date 1446297389 -3600
# Node ID 053f7083b3ebdcb58aa17b72ac330f3a0a66bd06
# Parent  d05f3d86a758931d5cd379b9ec86b766eebb20da
global start time as reference point;

diff -r d05f3d86a758 -r 053f7083b3eb 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])