# HG changeset patch
# User wenzelm
# Date 1493328976 -7200
# Node ID b408ca224954757d71059ab53da1a132603c2ab2
# Parent  7fffa01b2d2b01830b9c0e3cbf50a0087dd999b2
more encode/decode operations;

diff -r 7fffa01b2d2b -r b408ca224954 src/Pure/General/time.scala
--- 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
diff -r 7fffa01b2d2b -r b408ca224954 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Thu Apr 27 22:21:43 2017 +0200
+++ b/src/Pure/General/timing.scala	Thu Apr 27 23:36:16 2017 +0200
@@ -29,6 +29,19 @@
       Exn.release(result)
     }
     else e
+
+  val encode: XML.Encode.T[Timing] = (t: Timing) =>
+  {
+    import XML.Encode._
+    triple(Time.encode, Time.encode, Time.encode)(t.elapsed, t.cpu, t.gc)
+  }
+
+  val decode: XML.Decode.T[Timing] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val (elapsed, cpu, gc) = triple(Time.decode, Time.decode, Time.decode)(body)
+    Timing(elapsed, cpu, gc)
+  }
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)