clarified signature;
authorwenzelm
Fri Mar 23 16:07:20 2018 +0100 (15 months ago ago)
changeset 6793204352338f7f3
parent 67931 f7917c15b566
child 67933 604da273e18d
clarified signature;
src/Pure/General/timing.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     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;
     2.1 --- a/src/Pure/Isar/proof.ML	Fri Mar 23 14:04:50 2018 +0100
     2.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 23 16:07:20 2018 +0100
     2.3 @@ -1303,12 +1303,9 @@
     2.4  fun future_terminal_proof proof1 proof2 done state =
     2.5    if Goal.future_enabled 3 andalso not (is_relevant state) then
     2.6      state |> future_proof (fn state' =>
     2.7 -      let
     2.8 -        val pos = Position.thread_data ();
     2.9 -        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
    2.10 -      in
    2.11 +      let val pos = Position.thread_data () in
    2.12          Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
    2.13 -          (fn () => ((), Timing.protocol props proof2 state'))
    2.14 +          (fn () => ((), Timing.protocol "by" pos proof2 state'))
    2.15        end) |> snd |> done
    2.16    else proof1 state;
    2.17  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 23 14:04:50 2018 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 23 16:07:20 2018 +0100
     3.3 @@ -584,15 +584,9 @@
     3.4  local
     3.5  
     3.6  fun app int (tr as Transition {trans, ...}) =
     3.7 -  setmp_thread_position tr (fn state =>
     3.8 -    let
     3.9 -      val timing_start = Timing.start ();
    3.10 -      val (result, opt_err) = apply_trans int trans state;
    3.11 -      val timing_result = Timing.result timing_start;
    3.12 -      val timing_props =
    3.13 -        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    3.14 -      val _ = Timing.protocol_message timing_props timing_result;
    3.15 -    in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
    3.16 +  setmp_thread_position tr
    3.17 +    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
    3.18 +      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
    3.19  
    3.20  in
    3.21