# HG changeset patch
# User wenzelm
# Date 1357131059 -3600
# Node ID 34b109c5324cda086f31f156a990d329d1859d67
# Parent  a0888c03a727e6205f12f009fb57d8e656663c51
inline ML statistics into build log;

diff -r a0888c03a727 -r 34b109c5324c src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jan 02 13:20:10 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 02 13:50:59 2013 +0100
@@ -204,7 +204,7 @@
         ("workers_waiting", Markup.print_int waiting)] @
         ML_Statistics.get ();
     in
-      Output.protocol_message (Markup.ML_statistics @ stats) ""
+      Output.protocol_message (Markup.ML_statistics :: stats) ""
         handle Fail msg => warning msg
     end
   else ();
diff -r a0888c03a727 -r 34b109c5324c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Jan 02 13:20:10 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Jan 02 13:50:59 2013 +0100
@@ -130,7 +130,7 @@
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
-  val ML_statistics: Properties.T
+  val ML_statistics: string * string
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -402,7 +402,7 @@
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
-val ML_statistics = [(functionN, "ML_statistics")];
+val ML_statistics = (functionN, "ML_statistics");
 
 
 
diff -r a0888c03a727 -r 34b109c5324c src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Wed Jan 02 13:20:10 2013 +0100
+++ b/src/Pure/System/build.ML	Wed Jan 02 13:50:59 2013 +0100
@@ -12,6 +12,22 @@
 structure Build: BUILD =
 struct
 
+(* protocol messages *)
+
+fun ML_statistics (function :: stats) "" =
+      if function = Markup.ML_statistics then SOME stats
+      else NONE
+  | ML_statistics _ _ = NONE;
+
+fun protocol_message props output =
+  (case ML_statistics props output of
+    SOME stats =>
+      writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
+  | NONE => raise Fail "Undefined Output.protocol_message");
+
+
+(* build *)
+
 local
 
 fun no_document options =
@@ -87,6 +103,7 @@
         theories |>
           (List.app use_theories
             |> Session.with_timing name verbose
+            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();