1.1 --- a/src/Pure/General/markup.ML	Sat Nov 06 17:55:32 2010 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Sat Nov 06 18:10:35 2010 +0100
     1.3 @@ -99,7 +99,10 @@
     1.4    val command_spanN: string val command_span: string -> T
     1.5    val ignored_spanN: string val ignored_span: T
     1.6    val malformed_spanN: string val malformed_span: T
     1.7 -  val timing: timing -> T
     1.8 +  val elapsedN: string
     1.9 +  val cpuN: string
    1.10 +  val gcN: string
    1.11 +  val timingN: string val timing: timing -> T
    1.12    val subgoalsN: string
    1.13    val proof_stateN: string val proof_state: int -> T
    1.14    val stateN: string val state: T
    1.15 @@ -306,11 +309,21 @@
    1.16  val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
    1.17  
    1.18  
    1.19 -(* toplevel *)
    1.20 +(* timing *)
    1.21 +
    1.22 +val timingN = "timing";
    1.23 +val elapsedN = "elapsed";
    1.24 +val cpuN = "cpu";
    1.25 +val gcN = "gc";
    1.26  
    1.27  fun timing ({elapsed, cpu, gc, ...}: timing) =
    1.28 -  ("timing",
    1.29 -    [("elapsed", Time.toString elapsed), ("cpu", Time.toString cpu), ("gc", Time.toString gc)]);
    1.30 +  (timingN,
    1.31 +   [(elapsedN, Time.toString elapsed),
    1.32 +    (cpuN, Time.toString cpu),
    1.33 +    (gcN, Time.toString gc)]);
    1.34 +
    1.35 +
    1.36 +(* toplevel *)
    1.37  
    1.38  val subgoalsN = "subgoals";
    1.39  val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;

     2.1 --- a/src/Pure/General/markup.scala	Sat Nov 06 17:55:32 2010 +0100
     2.2 +++ b/src/Pure/General/markup.scala	Sat Nov 06 18:10:35 2010 +0100
     2.3 @@ -216,6 +216,31 @@
     2.4    val MALFORMED_SPAN = "malformed_span"
     2.5  
     2.6  
     2.7 +  /* timing */
     2.8 +
     2.9 +  val TIMING = "timing"
    2.10 +  val ELAPSED = "elapsed"
    2.11 +  val CPU = "cpu"
    2.12 +  val GC = "gc"
    2.13 +
    2.14 +  object Timing
    2.15 +  {
    2.16 +    def apply(timing: isabelle.Timing): Markup =
    2.17 +      Markup(TIMING, List(
    2.18 +        (ELAPSED, Double(timing.elapsed)),
    2.19 +        (CPU, Double(timing.cpu)),
    2.20 +        (GC, Double(timing.gc))))
    2.21 +    def unapply(markup: Markup): Option[isabelle.Timing] =
    2.22 +      markup match {
    2.23 +        case Markup(TIMING, List(
    2.24 +          (ELAPSED, Double(elapsed)),
    2.25 +          (CPU, Double(cpu)),
    2.26 +          (GC, Double(gc)))) => Some(isabelle.Timing(elapsed, cpu, gc))
    2.27 +        case _ => None
    2.28 +      }
    2.29 +  }
    2.30 +
    2.31 +
    2.32    /* toplevel */
    2.33  
    2.34    val SUBGOALS = "subgoals"