src/Pure/General/timing.scala

   {
     import XML.Decode._
     val (elapsed, cpu, gc) = triple(Time.decode, Time.decode, Time.decode)(body)
     Timing(elapsed, cpu, gc)
   }
+
+  def write(t: Timing): Bytes =
+    if (t.is_zero) Bytes.empty
+    else Bytes(YXML.string_of_body(encode(t)))
+
+  def read(bs: Bytes): Timing =
+    if (bs.isEmpty) zero
+    else decode(YXML.parse_body(bs.text))
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
 {
   def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero