src/Pure/General/time.scala
changeset 61528 053f7083b3eb
parent 57912 dd9550f84106
child 61602 a2f0f659a3c2
equal deleted inserted replaced
61527:d05f3d86a758 61528:053f7083b3eb
    13 
    13 
    14 object Time
    14 object Time
    15 {
    15 {
    16   def seconds(s: Double): Time = new Time((s * 1000.0).round)
    16   def seconds(s: Double): Time = new Time((s * 1000.0).round)
    17   def ms(m: Long): Time = new Time(m)
    17   def ms(m: Long): Time = new Time(m)
       
    18   def now(): Time = ms(System.currentTimeMillis())
       
    19 
    18   val zero: Time = ms(0)
    20   val zero: Time = ms(0)
    19   def now(): Time = ms(System.currentTimeMillis())
    21   val start: Time = now()
    20 
    22 
    21   def print_seconds(s: Double): String =
    23   def print_seconds(s: Double): String =
    22     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    24     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    23 }
    25 }
    24 
    26