--- 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
--- 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)