added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);

--- a/src/Pure/Concurrent/future.ML	Fri Jan 18 00:18:11 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Jan 18 16:20:09 2013 +0100
@@ -52,6 +52,7 @@
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val ML_statistics: bool Unsynchronized.ref
+  val forked_proofs: int Unsynchronized.ref
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -187,6 +188,7 @@
 (* status *)
 
 val ML_statistics = Unsynchronized.ref false;
+val forked_proofs = Unsynchronized.ref 0;
 
 fun report_status () = (*requires SYNCHRONIZED*)
   if ! ML_statistics then
@@ -197,6 +199,7 @@
       val waiting = count_workers Waiting;
       val stats =
        [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+        ("tasks_proof", Markup.print_int (! forked_proofs)),
         ("tasks_ready", Markup.print_int ready),
         ("tasks_pending", Markup.print_int pending),
         ("tasks_running", Markup.print_int running),

--- a/src/Pure/ML/ml_statistics.scala	Fri Jan 18 00:18:11 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Jan 18 16:20:09 2013 +0100
@@ -43,7 +43,8 @@
     ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
 
   val tasks_fields =
-    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+    ("Future tasks",
+      List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
 
   val workers_fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))

--- a/src/Pure/goal.ML	Fri Jan 18 00:18:11 2013 +0100
+++ b/src/Pure/goal.ML	Fri Jan 18 16:20:09 2013 +0100
@@ -116,9 +116,7 @@
   Synchronized.change forked_proofs (fn (m, groups, tab) =>
     let
       val n = m + i;
-      val _ =
-        Multithreading.tracing 2 (fn () =>
-          ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
+      val _ = Future.forked_proofs := n;
     in (n, groups, tab) end);
 
 fun register_forked id future =
@@ -176,7 +174,7 @@
 
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
-    (groups, (0, [], Inttab.empty)));
+    (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
 end;