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])