--- a/src/Pure/PIDE/markup.ML Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Feb 19 12:58:32 2013 +0100
@@ -92,6 +92,7 @@
val elapsedN: string
val cpuN: string
val gcN: string
+ val timing_propertiesN: string list
val timing_properties: Timing.timing -> Properties.T
val timingN: string val timing: Timing.timing -> T
val subgoalsN: string
@@ -333,6 +334,8 @@
val cpuN = "cpu";
val gcN = "gc";
+val timing_propertiesN = [elapsedN, cpuN, gcN];
+
fun timing_properties {elapsed, cpu, gc} =
[(elapsedN, Time.toString elapsed),
(cpuN, Time.toString cpu),