src/Pure/PIDE/markup.ML

--- a/src/Pure/PIDE/markup.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Jan 09 13:38:57 2013 +0100
@@ -92,6 +92,7 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
+  val timing_properties: Timing.timing -> Properties.T
   val timingN: string val timing: Timing.timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
@@ -323,16 +324,17 @@
 
 (* timing *)
 
-val timingN = "timing";
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
-fun timing {elapsed, cpu, gc} =
-  (timingN,
-   [(elapsedN, Time.toString elapsed),
-    (cpuN, Time.toString cpu),
-    (gcN, Time.toString gc)]);
+fun timing_properties {elapsed, cpu, gc} =
+ [(elapsedN, Time.toString elapsed),
+  (cpuN, Time.toString cpu),
+  (gcN, Time.toString gc)];
+
+val timingN = "timing";
+fun timing t = (timingN, timing_properties t);
 
 
 (* toplevel *)