record total number of tasks;

--- 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 ();

--- a/src/Pure/Concurrent/task_queue.ML	Wed May 09 15:07:20 2018 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Wed May 09 19:53:37 2018 +0200
@@ -32,7 +32,9 @@
   val group_tasks: queue -> group list -> task list
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
-  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
+  val total_jobs: queue -> int
+  val status: queue ->
+    {ready: int, pending: int, running: int, passive: int, urgent: int, total: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
@@ -217,10 +219,12 @@
 
 (* queue *)
 
-datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int};
+datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int, total: int};
 
-fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
-val empty = make_queue Inttab.empty Task_Graph.empty 0;
+fun make_queue groups jobs urgent total =
+  Queue {groups = groups, jobs = jobs, urgent = urgent, total = total};
+
+val empty = make_queue Inttab.empty Task_Graph.empty 0 0;
 
 fun group_tasks (Queue {groups, ...}) gs =
   fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g)))
@@ -249,10 +253,12 @@
 
 fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs);
 
+fun total_jobs (Queue {total, ...}) = total;
+
 
 (* queue status *)
 
-fun status (Queue {jobs, urgent, ...}) =
+fun status (Queue {jobs, urgent, total, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -261,7 +267,7 @@
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
-  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
+  in {ready = x, pending = y, running = z, passive = w, urgent = urgent, total = total} end;
 
 
 
@@ -295,35 +301,38 @@
 
 (* finish *)
 
-fun finish task (Queue {groups, jobs, urgent}) =
+fun finish task (Queue {groups, jobs, urgent, total}) =
   let
     val group = group_of_task task;
     val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
     val jobs' = Task_Graph.del_node task jobs;
+    val total' = total - 1;
     val maximal = Task_Graph.is_maximal jobs task;
-  in (maximal, make_queue groups' jobs' urgent) end;
+  in (maximal, make_queue groups' jobs' urgent total') end;
 
 
 (* enroll *)
 
-fun enroll thread name group (Queue {groups, jobs, urgent}) =
+fun enroll thread name group (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Running thread);
-  in (task, make_queue groups' jobs' urgent) end;
+    val total' = total + 1;
+  in (task, make_queue groups' jobs' urgent total') end;
 
 
 (* enqueue *)
 
-fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
+fun enqueue_passive group name abort (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
-  in (task, make_queue groups' jobs' urgent) end;
+    val total' = total + 1;
+  in (task, make_queue groups' jobs' urgent total') end;
 
-fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
+fun enqueue name group deps pri job (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name (SOME pri);
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
@@ -331,39 +340,40 @@
       |> Task_Graph.new_node (task, Job [job])
       |> fold (add_job task) deps;
     val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
-  in (task, make_queue groups' jobs' urgent') end;
+    val total' = total + 1;
+  in (task, make_queue groups' jobs' urgent' total') end;
 
-fun extend task job (Queue {groups, jobs, urgent}) =
+fun extend task job (Queue {groups, jobs, urgent, total}) =
   (case try (get_job jobs) task of
-    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent)
+    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent total)
   | _ => NONE);
 
 
 (* dequeue *)
 
-fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) =
+fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent, total}) =
   (case try (get_job jobs) task of
     SOME (Passive _) =>
       let val jobs' = set_job task (Running thread) jobs
-      in (SOME true, make_queue groups jobs' urgent) end
+      in (SOME true, make_queue groups jobs' urgent total) end
   | SOME _ => (SOME false, queue)
   | NONE => (NONE, queue));
 
-fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) =
+fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent, total}) =
   if not urgent_only orelse urgent > 0 then
     (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of
       SOME (result as (task, _)) =>
         let
           val jobs' = set_job task (Running thread) jobs;
           val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
-        in (SOME result, make_queue groups jobs' urgent') end
+        in (SOME result, make_queue groups jobs' urgent' total) end
     | NONE => (NONE, queue))
   else (NONE, queue);
 
 
 (* dequeue wrt. dynamic dependencies *)
 
-fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) =
+fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent, total}) =
   let
     fun ready [] rest = (NONE, rev rest)
       | ready (task :: tasks) rest =
@@ -388,7 +398,7 @@
       let
         val jobs' = set_job task (Running thread) jobs;
         val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
-      in ((SOME res, deps'), make_queue groups jobs' urgent') end;
+      in ((SOME res, deps'), make_queue groups jobs' urgent' total) end;
   in
     (case ready deps [] of
       (SOME res, deps') => result res deps'

--- a/src/Pure/ML/ml_statistics.scala	Wed May 09 15:07:20 2018 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Wed May 09 19:53:37 2018 +0200
@@ -39,7 +39,8 @@
 
   val tasks_fields: Fields =
     ("Future tasks",
-      List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
+      List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
+        "tasks_urgent", "tasks_total"))
 
   val workers_fields: Fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))