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

     2.1 --- a/src/Pure/PIDE/markup.ML	Mon Feb 18 18:34:55 2013 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 10:55:11 2013 +0100
     2.3 @@ -135,6 +135,7 @@
     2.4    val cancel_scala: string -> Properties.T
     2.5    val ML_statistics: Properties.entry
     2.6    val task_statistics: Properties.entry
     2.7 +  val command_timing: Properties.entry
     2.8    val loading_theory: string -> Properties.T
     2.9    val dest_loading_theory: Properties.T -> string option
    2.10    val no_output: Output.output * Output.output
    2.11 @@ -415,6 +416,8 @@
    2.12  
    2.13  val task_statistics = (functionN, "task_statistics");
    2.14  
    2.15 +val command_timing = (functionN, "command_timing");
    2.16 +
    2.17  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    2.18  
    2.19  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name

     3.1 --- a/src/Pure/Tools/build.ML	Mon Feb 18 18:34:55 2013 +0100
     3.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 10:55:11 2013 +0100
     3.3 @@ -16,30 +16,23 @@
     3.4  
     3.5  local
     3.6  
     3.7 -fun ML_statistics (function :: stats) "" =
     3.8 -      if function = Markup.ML_statistics then SOME stats
     3.9 -      else NONE
    3.10 -  | ML_statistics _ _ = NONE;
    3.11 +(* FIXME avoid hardwired stuff!? *)
    3.12 +val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    3.13  
    3.14 -fun task_statistics (function :: stats) "" =
    3.15 -      if function = Markup.task_statistics then SOME stats
    3.16 -      else NONE
    3.17 -  | task_statistics _ _ = NONE;
    3.18 -
    3.19 -val print_properties = YXML.string_of_body o XML.Encode.properties;
    3.20 +fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    3.21  
    3.22  in
    3.23  
    3.24  fun protocol_message props output =
    3.25 -  (case ML_statistics props output of
    3.26 -    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
    3.27 -  | NONE =>
    3.28 -      (case task_statistics props output of
    3.29 -        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
    3.30 -      | NONE =>
    3.31 -          (case Markup.dest_loading_theory props of
    3.32 -            SOME name => writeln ("\floading_theory = " ^ name)
    3.33 -          | NONE => raise Fail "Undefined Output.protocol_message")));
    3.34 +  (case props of
    3.35 +    function :: args =>
    3.36 +      if member (op =) protocol_echo function then
    3.37 +        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    3.38 +      else
    3.39 +        (case Markup.dest_loading_theory props of
    3.40 +          SOME name => writeln ("\floading_theory = " ^ name)
    3.41 +        | NONE => protocol_undef ())
    3.42 +  | [] => protocol_undef ());
    3.43  
    3.44  end;
    3.45