1.1 --- a/src/Pure/Concurrent/future.ML	Fri Jan 18 00:18:11 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Jan 18 16:20:09 2013 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    val peek: 'a future -> 'a Exn.result option
     1.5    val is_finished: 'a future -> bool
     1.6    val ML_statistics: bool Unsynchronized.ref
     1.7 +  val forked_proofs: int Unsynchronized.ref
     1.8    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.9    val cancel_group: group -> unit
    1.10    val cancel: 'a future -> unit
    1.11 @@ -187,6 +188,7 @@
    1.12  (* status *)
    1.13  
    1.14  val ML_statistics = Unsynchronized.ref false;
    1.15 +val forked_proofs = Unsynchronized.ref 0;
    1.16  
    1.17  fun report_status () = (*requires SYNCHRONIZED*)
    1.18    if ! ML_statistics then
    1.19 @@ -197,6 +199,7 @@
    1.20        val waiting = count_workers Waiting;
    1.21        val stats =
    1.22         [("now", signed_string_of_real (Time.toReal (Time.now ()))),
    1.23 +        ("tasks_proof", Markup.print_int (! forked_proofs)),
    1.24          ("tasks_ready", Markup.print_int ready),
    1.25          ("tasks_pending", Markup.print_int pending),
    1.26          ("tasks_running", Markup.print_int running),

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

     3.1 --- a/src/Pure/goal.ML	Fri Jan 18 00:18:11 2013 +0100
     3.2 +++ b/src/Pure/goal.ML	Fri Jan 18 16:20:09 2013 +0100
     3.3 @@ -116,9 +116,7 @@
     3.4    Synchronized.change forked_proofs (fn (m, groups, tab) =>
     3.5      let
     3.6        val n = m + i;
     3.7 -      val _ =
     3.8 -        Multithreading.tracing 2 (fn () =>
     3.9 -          ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
    3.10 +      val _ = Future.forked_proofs := n;
    3.11      in (n, groups, tab) end);
    3.12  
    3.13  fun register_forked id future =
    3.14 @@ -176,7 +174,7 @@
    3.15  
    3.16  fun reset_futures () =
    3.17    Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
    3.18 -    (groups, (0, [], Inttab.empty)));
    3.19 +    (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
    3.20  
    3.21  end;
    3.22