src/Pure/General/time.scala
changeset 57912 dd9550f84106
parent 56691 ad5d7461b370
child 61528 053f7083b3eb
equal deleted inserted replaced
57911:dcb758188aa6 57912:dd9550f84106
    38   def max(t: Time): Time = if (this > t) this else t
    38   def max(t: Time): Time = if (this > t) this else t
    39 
    39 
    40   def is_zero: Boolean = ms == 0
    40   def is_zero: Boolean = ms == 0
    41   def is_relevant: Boolean = ms >= 1
    41   def is_relevant: Boolean = ms >= 1
    42 
    42 
    43   override def toString = Time.print_seconds(seconds)
    43   override def toString: String = Time.print_seconds(seconds)
    44 
    44 
    45   def message: String = toString + "s"
    45   def message: String = toString + "s"
    46 }
    46 }
    47 
    47