# HG changeset patch
# User wenzelm
# Date 1521817640 -3600
# Node ID 04352338f7f35fb48e6fc8c56fb8c354da6894c3
# Parent  f7917c15b566c8b415da783af66a316b3f83c3d0
clarified signature;

diff -r f7917c15b566 -r 04352338f7f3 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Fri Mar 23 14:04:50 2018 +0100
+++ b/src/Pure/General/timing.ML	Fri Mar 23 16:07:20 2018 +0100
@@ -23,8 +23,8 @@
   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 =
@@ -103,15 +103,16 @@
 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;
diff -r f7917c15b566 -r 04352338f7f3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Mar 23 14:04:50 2018 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 23 16:07:20 2018 +0100
@@ -1303,12 +1303,9 @@
 fun future_terminal_proof proof1 proof2 done state =
   if Goal.future_enabled 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
-      let
-        val pos = Position.thread_data ();
-        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
-      in
+      let val pos = Position.thread_data () in
         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
-          (fn () => ((), Timing.protocol props proof2 state'))
+          (fn () => ((), Timing.protocol "by" pos proof2 state'))
       end) |> snd |> done
   else proof1 state;
 
diff -r f7917c15b566 -r 04352338f7f3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 23 14:04:50 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Mar 23 16:07:20 2018 +0100
@@ -584,15 +584,9 @@
 local
 
 fun app int (tr as Transition {trans, ...}) =
-  setmp_thread_position tr (fn state =>
-    let
-      val timing_start = Timing.start ();
-      val (result, opt_err) = apply_trans int trans state;
-      val timing_result = Timing.result timing_start;
-      val timing_props =
-        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
-      val _ = Timing.protocol_message timing_props timing_result;
-    in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
+  setmp_thread_position tr
+    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
+      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
 
 in