src/Pure/PIDE/markup.ML
changeset 45674 eb65c9d17e2f
parent 45670 b84170538043
child 46894 e2ad717ec889
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Nov 29 21:29:53 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Nov 29 21:50:00 2011 +0100
     1.3 @@ -15,10 +15,6 @@
     1.4    val nameN: string
     1.5    val name: string -> T -> T
     1.6    val kindN: string
     1.7 -  val elapsedN: string
     1.8 -  val cpuN: string
     1.9 -  val gcN: string
    1.10 -  val timingN: string val timing: Timing.timing -> T
    1.11    val no_output: Output.output * Output.output
    1.12    val default_output: T -> Output.output * Output.output
    1.13    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    1.14 @@ -67,20 +63,6 @@
    1.15  val kindN = "kind";
    1.16  
    1.17  
    1.18 -(* timing *)
    1.19 -
    1.20 -val timingN = "timing";
    1.21 -val elapsedN = "elapsed";
    1.22 -val cpuN = "cpu";
    1.23 -val gcN = "gc";
    1.24 -
    1.25 -fun timing {elapsed, cpu, gc} =
    1.26 -  (timingN,
    1.27 -   [(elapsedN, Time.toString elapsed),
    1.28 -    (cpuN, Time.toString cpu),
    1.29 -    (gcN, Time.toString gc)]);
    1.30 -
    1.31 -
    1.32  
    1.33  (** print mode operations **)
    1.34