# HG changeset patch
# User wenzelm
# Date 1361267711 -3600
# Node ID e6e7685fc8f84859a1dddb276eadcecd985c5ae1
# Parent  d0fa18638478e3f88a6c21facdee14290d40034c
emit command_timing properties into build log;
tuned;

diff -r d0fa18638478 -r e6e7685fc8f8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 10:55:11 2013 +0100
@@ -612,12 +612,22 @@
 
 local
 
+fun timing_message tr t =
+  if Timing.is_relevant t then
+    Output.protocol_message
+      (Markup.command_timing :: (Markup.nameN, name_of tr) ::
+        Position.properties_of (pos_of tr) @ Markup.timing_properties t) ""
+    handle Fail _ => ()
+  else ();
+
 fun app int (tr as Transition {trans, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
     let
       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
       fun do_profiling f x = profile (! profiling) f x;
 
+      val start = Timing.start ();
+
       val (result, status) =
          state |>
           (apply_trans int trans
@@ -625,6 +635,8 @@
             |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
 
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
+
+      val _ = timing_message tr (Timing.result start);
     in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
 
 in
diff -r d0fa18638478 -r e6e7685fc8f8 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 10:55:11 2013 +0100
@@ -135,6 +135,7 @@
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
+  val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val no_output: Output.output * Output.output
@@ -415,6 +416,8 @@
 
 val task_statistics = (functionN, "task_statistics");
 
+val command_timing = (functionN, "command_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
diff -r d0fa18638478 -r e6e7685fc8f8 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/Tools/build.ML	Tue Feb 19 10:55:11 2013 +0100
@@ -16,30 +16,23 @@
 
 local
 
-fun ML_statistics (function :: stats) "" =
-      if function = Markup.ML_statistics then SOME stats
-      else NONE
-  | ML_statistics _ _ = NONE;
+(* FIXME avoid hardwired stuff!? *)
+val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
 
-fun task_statistics (function :: stats) "" =
-      if function = Markup.task_statistics then SOME stats
-      else NONE
-  | task_statistics _ _ = NONE;
-
-val print_properties = YXML.string_of_body o XML.Encode.properties;
+fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
 
 in
 
 fun protocol_message props output =
-  (case ML_statistics props output of
-    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
-  | NONE =>
-      (case task_statistics props output of
-        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
-      | NONE =>
-          (case Markup.dest_loading_theory props of
-            SOME name => writeln ("\floading_theory = " ^ name)
-          | NONE => raise Fail "Undefined Output.protocol_message")));
+  (case props of
+    function :: args =>
+      if member (op =) protocol_echo function then
+        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+      else
+        (case Markup.dest_loading_theory props of
+          SOME name => writeln ("\floading_theory = " ^ name)
+        | NONE => protocol_undef ())
+  | [] => protocol_undef ());
 
 end;