src/Pure/PIDE/markup.scala
changeset 51662 3391a493f39a
parent 51574 2b58d7b139d6
child 51818 517f232e867d
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Apr 09 15:59:02 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Apr 09 20:16:52 2013 +0200
     1.3 @@ -193,6 +193,7 @@
     1.4    {
     1.5      def apply(timing: isabelle.Timing): Properties.T =
     1.6        Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
     1.7 +
     1.8      def unapply(props: Properties.T): Option[isabelle.Timing] =
     1.9        (props, props, props) match {
    1.10          case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
    1.11 @@ -206,6 +207,7 @@
    1.12    object Timing
    1.13    {
    1.14      def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
    1.15 +
    1.16      def unapply(markup: Markup): Option[isabelle.Timing] =
    1.17        markup match {
    1.18          case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
    1.19 @@ -214,6 +216,22 @@
    1.20    }
    1.21  
    1.22  
    1.23 +  /* command timing */
    1.24 +
    1.25 +  object Command_Timing
    1.26 +  {
    1.27 +    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
    1.28 +      props match {
    1.29 +        case (FUNCTION, "command_timing") :: args =>
    1.30 +          (args, args) match {
    1.31 +            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
    1.32 +            case _ => None
    1.33 +          }
    1.34 +        case _ => None
    1.35 +      }
    1.36 +  }
    1.37 +
    1.38 +
    1.39    /* toplevel */
    1.40  
    1.41    val SUBGOALS = "subgoals"