# HG changeset patch
# User wenzelm
# Date 1498134433 -7200
# Node ID c88d1c36c9c3b706f20f71b0d50638208d291313
# Parent  c6e9c7d140ffae7caadf582eceebbe0c74552c32
more informative task_statistics;

diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -148,7 +148,7 @@
   let
     val req: request Single_Assignment.var = Single_Assignment.var "request";
     fun abort () = ignore (cancel (Single_Assignment.await req));
-    val promise: unit future = Future.promise abort;
+    val promise: unit future = Future.promise_name "event_timer" abort;
     val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
   in promise end);
 
diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -37,7 +37,7 @@
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val promise_group: group -> (unit -> unit) -> 'a future
+  val promise_name: string -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
@@ -599,8 +599,9 @@
 
 (* promised futures -- fulfilled by external means *)
 
-fun promise_group group abort : 'a future =
+fun promise_name name abort : 'a future =
   let
+    val group = worker_subgroup ();
     val result = Single_Assignment.var "promise" : 'a result;
     fun assign () = assign_result group result Exn.interrupt_exn
       handle Fail _ => true
@@ -612,10 +613,10 @@
       Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
-      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
+      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job));
   in Future {promised = true, task = task, result = result} end;
 
-fun promise abort = promise_group (worker_subgroup ()) abort;
+fun promise abort = promise_name "passive" abort;
 
 fun fulfill_result (Future {promised, task, result}) res =
   if not promised then raise Fail "Not a promised future"
diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -66,7 +66,7 @@
           val (expr, x) =
             Synchronized.change_result var
               (fn Expr e =>
-                    let val x = Future.promise I
+                    let val x = Future.promise_name "lazy" I
                     in ((SOME e, x), Result x) end
                 | Result x => ((NONE, x), Result x));
         in
diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -37,7 +37,7 @@
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
   val enroll: Thread.thread -> string -> group -> queue -> task * queue
-  val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
+  val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
@@ -312,9 +312,9 @@
 
 (* enqueue *)
 
-fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
+fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
   let
-    val task = new_task group "passive" NONE;
+    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;
diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/PIDE/active.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -49,7 +49,7 @@
   let
     val i = serial ();
     fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
-    val promise = Future.promise abort : string future;
+    val promise = Future.promise_name "dialog" abort : string future;
     val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
     fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
   in (result_markup, promise) end;
diff -r c6e9c7d140ff -r c88d1c36c9c3 src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/Pure/System/invoke_scala.ML	Thu Jun 22 14:27:13 2017 +0200
@@ -31,7 +31,7 @@
   let
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
-    val promise = Future.promise abort : string future;
+    val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
   in promise end;