src/Pure/General/time.scala
changeset 56691 ad5d7461b370
parent 56351 1c735e46acf0
child 57912 dd9550f84106
     1.1 --- a/src/Pure/General/time.scala	Thu Apr 24 10:38:14 2014 +0200
     1.2 +++ b/src/Pure/General/time.scala	Thu Apr 24 11:01:14 2014 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    def seconds(s: Double): Time = new Time((s * 1000.0).round)
     1.5    def ms(m: Long): Time = new Time(m)
     1.6    val zero: Time = ms(0)
     1.7 +  def now(): Time = ms(System.currentTimeMillis())
     1.8  
     1.9    def print_seconds(s: Double): String =
    1.10      String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    1.11 @@ -23,12 +24,18 @@
    1.12  
    1.13  final class Time private(val ms: Long) extends AnyVal
    1.14  {
    1.15 -  def + (t: Time): Time = new Time(ms + t.ms)
    1.16 -
    1.17    def seconds: Double = ms / 1000.0
    1.18  
    1.19 -  def min(t: Time): Time = if (ms < t.ms) this else t
    1.20 -  def max(t: Time): Time = if (ms > t.ms) this else t
    1.21 +  def + (t: Time): Time = new Time(ms + t.ms)
    1.22 +  def - (t: Time): Time = new Time(ms - t.ms)
    1.23 +
    1.24 +  def < (t: Time): Boolean = ms < t.ms
    1.25 +  def <= (t: Time): Boolean = ms <= t.ms
    1.26 +  def > (t: Time): Boolean = ms > t.ms
    1.27 +  def >= (t: Time): Boolean = ms >= t.ms
    1.28 +
    1.29 +  def min(t: Time): Time = if (this < t) this else t
    1.30 +  def max(t: Time): Time = if (this > t) this else t
    1.31  
    1.32    def is_zero: Boolean = ms == 0
    1.33    def is_relevant: Boolean = ms >= 1