src/Pure/General/time.scala
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