src/Pure/Concurrent/future.ML

     Unsynchronized.ref Working));
 
 
 (* scheduler *)
 
+fun ML_statistics () =
+  if ! ML_Statistics.enabled then
+    (case ML_Statistics.get () of
+      [] => ()
+    | stats => Output.protocol_message (Markup.ML_statistics @ stats) "")
+  else ();
+
 val status_ticks = Unsynchronized.ref 0;
 
 val last_round = Unsynchronized.ref Time.zeroTime;
 val next_round = seconds 0.05;
 

 
     val _ =
       if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else ();
     val _ =
       if tick andalso ! status_ticks = 0 then
+       (ML_statistics ();
         Multithreading.tracing 1 (fn () =>
           let
             val {ready, pending, running, passive} = Task_Queue.status (! queue);
             val total = length (! workers);
             val active = count_workers Working;

               string_of_int running ^ " running, " ^
               string_of_int passive ^ " passive; " ^
               string_of_int total ^ " workers, " ^
               string_of_int active ^ " active, " ^
               string_of_int waiting ^ " waiting "
-          end)
+          end))
       else ();
 
     val _ =
       if forall (Thread.isActive o #1) (! workers) then ()
       else

 fun scheduler_loop () =
  (while
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do (); last_round := Time.zeroTime);
+  do (); last_round := Time.zeroTime; ML_statistics ());
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
 
 fun scheduler_check () = (*requires SYNCHRONIZED*)