--- 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),