src/Pure/General/timing.ML

   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
   val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
-  val protocol_message: Properties.T -> timing -> unit
-  val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
+  val protocol_message: string -> Position.T -> timing -> unit
+  val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
 end
 
 structure Timing: TIMING =
 struct
 

 
 fun timeit e = cond_timeit true "" e;
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
-fun protocol_message props t =
+fun protocol_message name pos t =
   if is_relevant t then
-    Output.try_protocol_message (props @ Markup.timing_properties t) []
+    let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
+    in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
   else ();
 
-fun protocol props f x =
+fun protocol name pos f x =
   let
     val (t, result) = timing (Exn.interruptible_capture f) x;
-    val _ = protocol_message props t;
+    val _ = protocol_message name pos t;
   in Exn.release result end;
 
 end;
 
 structure Basic_Timing: BASIC_TIMING = Timing;