# HG changeset patch
# User wenzelm
# Date 1354182325 -3600
# Node ID 0eb9b5d09f31fc682441ead2188d91bf3eed356c
# Parent  902ccccf2efa8c46f2338894c06b0fd1a3e3e50e
more uniform ML statistics;

diff -r 902ccccf2efa -r 0eb9b5d09f31 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Nov 29 10:45:25 2012 +0100
@@ -51,6 +51,7 @@
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
+  val ML_statistics: bool Unsynchronized.ref
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -169,6 +170,10 @@
 val max_active = Unsynchronized.ref 0;
 val worker_trend = Unsynchronized.ref 0;
 
+val status_ticks = Unsynchronized.ref 0;
+val last_round = Unsynchronized.ref Time.zeroTime;
+val next_round = seconds 0.05;
+
 datatype worker_state = Working | Waiting | Sleeping;
 val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
 
@@ -176,6 +181,32 @@
   fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
 
 
+
+(* status *)
+
+val ML_statistics = Unsynchronized.ref false;
+
+fun report_status () = (*requires SYNCHRONIZED*)
+  if ! ML_statistics then
+    let
+      val {ready, pending, running, passive} = Task_Queue.status (! queue);
+      val total = length (! workers);
+      val active = count_workers Working;
+      val waiting = count_workers Waiting;
+      val stats =
+       [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+        ("tasks_ready", Markup.print_int ready),
+        ("tasks_pending", Markup.print_int pending),
+        ("tasks_running", Markup.print_int running),
+        ("tasks_passive", Markup.print_int passive),
+        ("workers_total", Markup.print_int total),
+        ("workers_active", Markup.print_int active),
+        ("workers_waiting", Markup.print_int waiting)] @
+        ML_Statistics.get ();
+    in Output.protocol_message (Markup.ML_statistics @ stats) "" end
+  else ();
+
+
 (* cancellation primitives *)
 
 fun cancel_now group = (*requires SYNCHRONIZED*)
@@ -271,18 +302,6 @@
 
 (* 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;
-
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     val now = Time.now ();
@@ -290,30 +309,12 @@
     val _ = if tick then last_round := now else ();
 
 
-    (* queue and worker status *)
+    (* runtime status *)
 
     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;
-            val waiting = count_workers Waiting;
-          in
-            "SCHEDULE " ^ Time.toString now ^ ": " ^
-              string_of_int ready ^ " ready, " ^
-              string_of_int pending ^ " pending, " ^
-              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))
-      else ();
+      if tick andalso ! status_ticks = 0 then report_status () else ();
 
     val _ =
       if forall (Thread.isActive o #1) (! workers) then ()
@@ -400,7 +401,7 @@
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do (); last_round := Time.zeroTime; ML_statistics ());
+  do (); last_round := Time.zeroTime; report_status ());
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
@@ -665,11 +666,6 @@
   else ();
 
 
-(* queue status *)
-
-fun queue_status () = Task_Queue.status (! queue);
-
-
 (*final declarations of this structure!*)
 val map = map_future;
 
diff -r 902ccccf2efa -r 0eb9b5d09f31 src/Pure/ML/ml_statistics_dummy.ML
--- a/src/Pure/ML/ml_statistics_dummy.ML	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/ML/ml_statistics_dummy.ML	Thu Nov 29 10:45:25 2012 +0100
@@ -6,14 +6,12 @@
 
 signature ML_STATISTICS =
 sig
-  val enabled: bool Unsynchronized.ref
   val get: unit -> Properties.T
 end;
 
 structure ML_Statistics: ML_STATISTICS =
 struct
 
-val enabled = Unsynchronized.ref false;
 fun get () = [];
 
 end;
diff -r 902ccccf2efa -r 0eb9b5d09f31 src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Thu Nov 29 10:45:25 2012 +0100
@@ -6,15 +6,12 @@
 
 signature ML_STATISTICS =
 sig
-  val enabled: bool Unsynchronized.ref
   val get: unit -> Properties.T
 end;
 
 structure ML_Statistics: ML_STATISTICS =
 struct
 
-val enabled = Unsynchronized.ref false;
-
 fun get () =
   let
     val
@@ -37,8 +34,7 @@
       timeNonGCUser,
       userCounters = _} = PolyML.Statistics.getLocalStats ()
   in
-    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
-     ("full_GCs", Markup.print_int gcFullGCs),
+    [("full_GCs", Markup.print_int gcFullGCs),
      ("partial_GCs", Markup.print_int gcPartialGCs),
      ("size_allocation", Markup.print_int sizeAllocation),
      ("size_allocation_free", Markup.print_int sizeAllocationFree),
diff -r 902ccccf2efa -r 0eb9b5d09f31 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/System/build.ML	Thu Nov 29 10:45:25 2012 +0100
@@ -27,7 +27,7 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
-    |> Unsynchronized.setmp ML_Statistics.enabled (Options.bool options "ML_statistics")
+    |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
     |> no_document options ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
diff -r 902ccccf2efa -r 0eb9b5d09f31 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Nov 29 10:45:25 2012 +0100
@@ -217,7 +217,7 @@
   protocol_command "Isabelle_Process.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
-        ML_Statistics.enabled := Options.bool options "ML_statistics";
+        Future.ML_statistics := Options.bool options "ML_statistics";
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
         if Multithreading.max_threads_value () < 2