src/Pure/General/markup.ML

   val malformedN: string val malformed: T
   val tokenN: string val token: Properties.T -> T
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
-  val timing: timing -> T
+  val elapsedN: string
+  val cpuN: string
+  val gcN: string
+  val timingN: string val timing: timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T

 val (command_spanN, command_span) = markup_string "command_span" nameN;
 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
 
 
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
+
+fun timing ({elapsed, cpu, gc, ...}: timing) =
+  (timingN,
+   [(elapsedN, Time.toString elapsed),
+    (cpuN, Time.toString cpu),
+    (gcN, Time.toString gc)]);
+
+
 (* toplevel *)
-
-fun timing ({elapsed, cpu, gc, ...}: timing) =
-  ("timing",
-    [("elapsed", Time.toString elapsed), ("cpu", Time.toString cpu), ("gc", Time.toString gc)]);
 
 val subgoalsN = "subgoals";
 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
 
 val (stateN, state) = markup_elem "state";