author | wenzelm |
Sat, 31 Oct 2015 14:16:29 +0100 | |
changeset 61528 | 053f7083b3eb |
parent 61527 | d05f3d86a758 |
child 61529 | 82fc5a6231a2 |
--- 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])