src/Pure/General/time.scala
changeset 65597 b408ca224954
parent 64370 865b39487b5d
child 65616 b8738569b8db
equal deleted inserted replaced
65596:7fffa01b2d2b 65597:b408ca224954
    25 
    25 
    26   def print_seconds(s: Double): String =
    26   def print_seconds(s: Double): String =
    27     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    27     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    28 
    28 
    29   def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
    29   def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
       
    30 
       
    31   val encode: XML.Encode.T[Time] = (t: Time) => XML.Encode.long(t.ms)
       
    32   val decode: XML.Decode.T[Time] = (body: XML.Body) => ms(XML.Decode.long(body))
    30 }
    33 }
    31 
    34 
    32 final class Time private(val ms: Long) extends AnyVal
    35 final class Time private(val ms: Long) extends AnyVal
    33 {
    36 {
    34   def seconds: Double = ms / 1000.0
    37   def seconds: Double = ms / 1000.0