| changeset 65597 | b408ca224954 |
| parent 64370 | 865b39487b5d |
| child 65616 | b8738569b8db |
--- a/src/Pure/General/time.scala Thu Apr 27 22:21:43 2017 +0200 +++ b/src/Pure/General/time.scala Thu Apr 27 23:36:16 2017 +0200 @@ -27,6 +27,9 @@ String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef]) def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L) + + val encode: XML.Encode.T[Time] = (t: Time) => XML.Encode.long(t.ms) + val decode: XML.Decode.T[Time] = (body: XML.Body) => ms(XML.Decode.long(body)) } final class Time private(val ms: Long) extends AnyVal