src/Pure/PIDE/markup.ML

--- a/src/Pure/PIDE/markup.ML	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Nov 29 21:50:00 2011 +0100
@@ -15,10 +15,6 @@
   val nameN: string
   val name: string -> T -> T
   val kindN: string
-  val elapsedN: string
-  val cpuN: string
-  val gcN: string
-  val timingN: string val timing: Timing.timing -> T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -67,20 +63,6 @@
 val kindN = "kind";
 
 
-(* 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)]);
-
-
 
 (** print mode operations **)