src/Pure/General/timing.ML
changeset 67932 04352338f7f3
parent 67001 b34fbf33a7ea
     1.1 --- a/src/Pure/General/timing.ML	Fri Mar 23 14:04:50 2018 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Fri Mar 23 16:07:20 2018 +0100
     1.3 @@ -23,8 +23,8 @@
     1.4    val is_relevant_time: Time.time -> bool
     1.5    val is_relevant: timing -> bool
     1.6    val message: timing -> string
     1.7 -  val protocol_message: Properties.T -> timing -> unit
     1.8 -  val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
     1.9 +  val protocol_message: string -> Position.T -> timing -> unit
    1.10 +  val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
    1.11  end
    1.12  
    1.13  structure Timing: TIMING =
    1.14 @@ -103,15 +103,16 @@
    1.15  fun timeap f x = timeit (fn () => f x);
    1.16  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
    1.17  
    1.18 -fun protocol_message props t =
    1.19 +fun protocol_message name pos t =
    1.20    if is_relevant t then
    1.21 -    Output.try_protocol_message (props @ Markup.timing_properties t) []
    1.22 +    let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
    1.23 +    in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
    1.24    else ();
    1.25  
    1.26 -fun protocol props f x =
    1.27 +fun protocol name pos f x =
    1.28    let
    1.29      val (t, result) = timing (Exn.interruptible_capture f) x;
    1.30 -    val _ = protocol_message props t;
    1.31 +    val _ = protocol_message name pos t;
    1.32    in Exn.release result end;
    1.33  
    1.34  end;