--- a/src/Pure/Concurrent/future.ML Wed May 09 15:07:20 2018 +0100
+++ b/src/Pure/Concurrent/future.ML Wed May 09 19:53:37 2018 +0200
@@ -171,10 +171,10 @@
fun report_status () = (*requires SYNCHRONIZED*)
if ! ML_statistics then
let
- val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
- val total = length (! workers);
- val active = count_workers Working;
- val waiting = count_workers Waiting;
+ val {ready, pending, running, passive, urgent, total} = Task_Queue.status (! queue);
+ val workers_total = length (! workers);
+ val workers_active = count_workers Working;
+ val workers_waiting = count_workers Waiting;
val stats =
[("now", Value.print_real (Time.toReal (Time.now ()))),
("tasks_ready", Value.print_int ready),
@@ -182,9 +182,10 @@
("tasks_running", Value.print_int running),
("tasks_passive", Value.print_int passive),
("tasks_urgent", Value.print_int urgent),
- ("workers_total", Value.print_int total),
- ("workers_active", Value.print_int active),
- ("workers_waiting", Value.print_int waiting)] @
+ ("tasks_total", Value.print_int total),
+ ("workers_total", Value.print_int workers_total),
+ ("workers_active", Value.print_int workers_active),
+ ("workers_waiting", Value.print_int workers_waiting)] @
ML_Statistics.get ();
in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
else ();