src/Pure/General/time.scala
author wenzelm
Thu Apr 24 11:01:14 2014 +0200 (2014-04-24)
changeset 56691 ad5d7461b370
parent 56351 1c735e46acf0
child 57912 dd9550f84106
permissions -rw-r--r--
tuned signature, in accordance to ML version;
     1 /*  Title:      Pure/General/time.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Time based on milliseconds.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.util.Locale
    12 
    13 
    14 object Time
    15 {
    16   def seconds(s: Double): Time = new Time((s * 1000.0).round)
    17   def ms(m: Long): Time = new Time(m)
    18   val zero: Time = ms(0)
    19   def now(): Time = ms(System.currentTimeMillis())
    20 
    21   def print_seconds(s: Double): String =
    22     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    23 }
    24 
    25 final class Time private(val ms: Long) extends AnyVal
    26 {
    27   def seconds: Double = ms / 1000.0
    28 
    29   def + (t: Time): Time = new Time(ms + t.ms)
    30   def - (t: Time): Time = new Time(ms - t.ms)
    31 
    32   def < (t: Time): Boolean = ms < t.ms
    33   def <= (t: Time): Boolean = ms <= t.ms
    34   def > (t: Time): Boolean = ms > t.ms
    35   def >= (t: Time): Boolean = ms >= t.ms
    36 
    37   def min(t: Time): Time = if (this < t) this else t
    38   def max(t: Time): Time = if (this > t) this else t
    39 
    40   def is_zero: Boolean = ms == 0
    41   def is_relevant: Boolean = ms >= 1
    42 
    43   override def toString = Time.print_seconds(seconds)
    44 
    45   def message: String = toString + "s"
    46 }
    47