src/Pure/PIDE/markup.scala
changeset 45674 eb65c9d17e2f
parent 45673 cd41e3903fbf
child 49613 2f6986e2ef06
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Nov 29 21:29:53 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Nov 29 21:50:00 2011 +0100
     1.3 @@ -24,32 +24,6 @@
     1.4    val Empty = Markup("", Nil)
     1.5    val Data = Markup("data", Nil)
     1.6    val Broken = Markup("broken", Nil)
     1.7 -
     1.8 -
     1.9 -  /* timing */
    1.10 -
    1.11 -  val TIMING = "timing"
    1.12 -  val ELAPSED = "elapsed"
    1.13 -  val CPU = "cpu"
    1.14 -  val GC = "gc"
    1.15 -
    1.16 -  object Timing
    1.17 -  {
    1.18 -    def apply(timing: isabelle.Timing): Markup =
    1.19 -      Markup(TIMING, List(
    1.20 -        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    1.21 -        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    1.22 -        (GC, Properties.Value.Double(timing.gc.seconds))))
    1.23 -    def unapply(markup: Markup): Option[isabelle.Timing] =
    1.24 -      markup match {
    1.25 -        case Markup(TIMING, List(
    1.26 -          (ELAPSED, Properties.Value.Double(elapsed)),
    1.27 -          (CPU, Properties.Value.Double(cpu)),
    1.28 -          (GC, Properties.Value.Double(gc)))) =>
    1.29 -            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    1.30 -        case _ => None
    1.31 -      }
    1.32 -  }
    1.33  }
    1.34  
    1.35