src/Pure/Isar/toplevel.ML
changeset 67932 04352338f7f3
parent 67643 b846f7a11fda
child 68132 6fb85346cb79
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 23 14:04:50 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 23 16:07:20 2018 +0100
     1.3 @@ -584,15 +584,9 @@
     1.4  local
     1.5  
     1.6  fun app int (tr as Transition {trans, ...}) =
     1.7 -  setmp_thread_position tr (fn state =>
     1.8 -    let
     1.9 -      val timing_start = Timing.start ();
    1.10 -      val (result, opt_err) = apply_trans int trans state;
    1.11 -      val timing_result = Timing.result timing_start;
    1.12 -      val timing_props =
    1.13 -        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    1.14 -      val _ = Timing.protocol_message timing_props timing_result;
    1.15 -    in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
    1.16 +  setmp_thread_position tr
    1.17 +    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
    1.18 +      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
    1.19  
    1.20  in
    1.21