src/Pure/PIDE/markup.scala
changeset 50781 a0f22c2d60cc
parent 50715 8cfd585b9162
child 50975 73ec6ad6700e
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 09 12:22:09 2013 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 09 13:38:57 2013 +0100
     1.3 @@ -181,25 +181,30 @@
     1.4  
     1.5    /* timing */
     1.6  
     1.7 +  val Elapsed = new Properties.Double("elapsed")
     1.8 +  val CPU = new Properties.Double("cpu")
     1.9 +  val GC = new Properties.Double("gc")
    1.10 +
    1.11 +  object Timing_Properties
    1.12 +  {
    1.13 +    def apply(timing: isabelle.Timing): Properties.T =
    1.14 +      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
    1.15 +    def unapply(props: Properties.T): Option[isabelle.Timing] =
    1.16 +      (props, props, props) match {
    1.17 +        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
    1.18 +          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    1.19 +        case _ => None
    1.20 +      }
    1.21 +  }
    1.22 +
    1.23    val TIMING = "timing"
    1.24 -  val ELAPSED = "elapsed"
    1.25 -  val CPU = "cpu"
    1.26 -  val GC = "gc"
    1.27  
    1.28    object Timing
    1.29    {
    1.30 -    def apply(timing: isabelle.Timing): Markup =
    1.31 -      Markup(TIMING, List(
    1.32 -        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    1.33 -        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    1.34 -        (GC, Properties.Value.Double(timing.gc.seconds))))
    1.35 +    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
    1.36      def unapply(markup: Markup): Option[isabelle.Timing] =
    1.37        markup match {
    1.38 -        case Markup(TIMING, List(
    1.39 -          (ELAPSED, Properties.Value.Double(elapsed)),
    1.40 -          (CPU, Properties.Value.Double(cpu)),
    1.41 -          (GC, Properties.Value.Double(gc)))) =>
    1.42 -            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    1.43 +        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
    1.44          case _ => None
    1.45        }
    1.46    }