src/Pure/Isar/toplevel.ML
changeset 51216 e6e7685fc8f8
parent 50917 9459f59cff09
child 51217 65ab2c4f4c32
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 18 18:34:55 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 10:55:11 2013 +0100
     1.3 @@ -612,12 +612,22 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun timing_message tr t =
     1.8 +  if Timing.is_relevant t then
     1.9 +    Output.protocol_message
    1.10 +      (Markup.command_timing :: (Markup.nameN, name_of tr) ::
    1.11 +        Position.properties_of (pos_of tr) @ Markup.timing_properties t) ""
    1.12 +    handle Fail _ => ()
    1.13 +  else ();
    1.14 +
    1.15  fun app int (tr as Transition {trans, print, no_timing, ...}) =
    1.16    setmp_thread_position tr (fn state =>
    1.17      let
    1.18        fun do_timing f x = (warning (command_msg "" tr); timeap f x);
    1.19        fun do_profiling f x = profile (! profiling) f x;
    1.20  
    1.21 +      val start = Timing.start ();
    1.22 +
    1.23        val (result, status) =
    1.24           state |>
    1.25            (apply_trans int trans
    1.26 @@ -625,6 +635,8 @@
    1.27              |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
    1.28  
    1.29        val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
    1.30 +
    1.31 +      val _ = timing_message tr (Timing.result start);
    1.32      in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
    1.33  
    1.34  in