# HG changeset patch
# User wenzelm
# Date 1493396698 -7200
# Node ID 823bbc467dfaa219865e9136ff3a3d667fef5bff
# Parent  b8738569b8dba462131795eff59430c45bdd1d41
unused;

diff -r b8738569b8db -r 823bbc467dfa src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Fri Apr 28 18:23:39 2017 +0200
+++ b/src/Pure/General/time.scala	Fri Apr 28 18:24:58 2017 +0200
@@ -27,9 +27,6 @@
     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 b8738569b8db -r 823bbc467dfa src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Fri Apr 28 18:23:39 2017 +0200
+++ b/src/Pure/General/timing.scala	Fri Apr 28 18:24:58 2017 +0200
@@ -29,27 +29,6 @@
       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)
-  }
-
-  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)