obsolete (see also 3391a493f39a);
authorwenzelm
Sat, 20 Sep 2025 16:39:35 +0200
changeset 83196 e8c2d64bb1d6
parent 83195 37e1d151be20
child 83197 7a2bd0d12f18
obsolete (see also 3391a493f39a);
src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Sep 20 16:34:32 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Sep 20 16:39:35 2025 +0200
@@ -208,7 +208,6 @@
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
-  val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
@@ -714,9 +713,6 @@
   (cpuN, Time.print cpu),
   (gcN, Time.print gc)];
 
-val timingN = "timing";
-fun timing t = (timingN, timing_properties t);
-
 
 (* command timing *)