src/Pure/General/time.scala
changeset 64056 ea528dc9962d
parent 64054 0edc966bee55
child 64370 865b39487b5d
equal deleted inserted replaced
64055:fd73e0019605 64056:ea528dc9962d
    25   val start: Time = now()
    25   val start: Time = now()
    26 
    26 
    27   def print_seconds(s: Double): String =
    27   def print_seconds(s: Double): String =
    28     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    28     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    29 
    29 
    30   def instant(t: Instant): Time = ms(t.getEpochSecond + t.getNano / 1000000L)
    30   def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
    31 }
    31 }
    32 
    32 
    33 final class Time private(val ms: Long) extends AnyVal
    33 final class Time private(val ms: Long) extends AnyVal
    34 {
    34 {
    35   def seconds: Double = ms / 1000.0
    35   def seconds: Double = ms / 1000.0