--- a/src/Pure/General/time.scala Thu Apr 24 10:38:14 2014 +0200
+++ b/src/Pure/General/time.scala Thu Apr 24 11:01:14 2014 +0200
@@ -16,6 +16,7 @@
def seconds(s: Double): Time = new Time((s * 1000.0).round)
def ms(m: Long): Time = new Time(m)
val zero: Time = ms(0)
+ def now(): Time = ms(System.currentTimeMillis())
def print_seconds(s: Double): String =
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
@@ -23,12 +24,18 @@
final class Time private(val ms: Long) extends AnyVal
{
- def + (t: Time): Time = new Time(ms + t.ms)
-
def seconds: Double = ms / 1000.0
- def min(t: Time): Time = if (ms < t.ms) this else t
- def max(t: Time): Time = if (ms > t.ms) this else t
+ def + (t: Time): Time = new Time(ms + t.ms)
+ def - (t: Time): Time = new Time(ms - t.ms)
+
+ def < (t: Time): Boolean = ms < t.ms
+ def <= (t: Time): Boolean = ms <= t.ms
+ def > (t: Time): Boolean = ms > t.ms
+ def >= (t: Time): Boolean = ms >= t.ms
+
+ def min(t: Time): Time = if (this < t) this else t
+ def max(t: Time): Time = if (this > t) this else t
def is_zero: Boolean = ms == 0
def is_relevant: Boolean = ms >= 1