# HG changeset patch
# User wenzelm
# Date 1296511021 -3600
# Node ID 1c191a39549f144f15c1d0a0f8422ac7c063d9f0
# Parent  2f70b1ddd09fe2cb7d34307bc366665e8acfdc09
support named tasks, for improved tracing;

diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -44,7 +44,8 @@
   val group_of: 'a future -> group
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val bulk: {group: group option, deps: task list, pri: int} -> (unit -> 'a) list -> 'a future list
+  val bulk: {name: string, group: group option, deps: task list, pri: int} ->
+    (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
@@ -399,7 +400,7 @@
 
 (* fork *)
 
-fun bulk {group, deps, pri} es =
+fun bulk {name, group, deps, pri} es =
   let
     val grp =
       (case group of
@@ -408,7 +409,7 @@
     fun enqueue e (minimal, queue) =
       let
         val (result, job) = future_job grp e;
-        val ((task, minimal'), queue') = Task_Queue.enqueue grp deps pri job queue;
+        val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
         val future = Future {promised = false, task = task, group = grp, result = result};
       in (future, (minimal orelse minimal', queue')) end;
   in
@@ -423,7 +424,7 @@
       in futures end)
   end;
 
-fun fork_pri pri e = singleton (bulk {group = NONE, deps = [], pri = pri}) e;
+fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
 fun fork e = fork_pri 0 e;
 
 
@@ -499,7 +500,9 @@
   in
     if extended then Future {promised = false, task = task, group = group, result = result}
     else
-      singleton (bulk {group = SOME group, deps = [task], pri = Task_Queue.pri_of_task task})
+      singleton
+        (bulk {name = "Future.map", group = SOME group,
+          deps = [task], pri = Task_Queue.pri_of_task task})
         (fn () => f (join x))
   end;
 
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -26,18 +26,19 @@
 structure Par_List: PAR_LIST =
 struct
 
-fun managed_results f xs =
+fun managed_results name f xs =
   if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
     let
       val group = Task_Queue.new_group (Future.worker_group ());
       val futures =
-        Future.bulk {group = SOME group, deps = [], pri = 0} (map (fn x => fn () => f x) xs);
+        Future.bulk {name = name, group = SOME group, deps = [], pri = 0}
+          (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     in results end
   else map (Exn.capture f) xs;
 
-fun map f xs = Exn.release_first (managed_results f xs);
+fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs);
 
 fun get_some f xs =
   let
@@ -45,7 +46,8 @@
     fun found (Exn.Exn (FOUND some)) = some
       | found _ = NONE;
     val results =
-      managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
+      managed_results "Par_List.get_some"
+        (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
   in
     (case get_first found results of
       SOME y => SOME y
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -28,7 +28,8 @@
   val cancel: queue -> group -> bool
   val cancel_all: queue -> group list
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
-  val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
+  val enqueue: string -> group -> task list -> int -> (bool -> bool) ->
+    queue -> (task * bool) * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
   val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
@@ -62,21 +63,26 @@
 
 (* tasks *)
 
-abstype task = Task of (int option * int) * timing Synchronized.var
+abstype task = Task of
+ {name: string,
+  id: int,
+  pri: int option,
+  timing: timing Synchronized.var}
 with
 
-val dummy_task = Task ((NONE, ~1), new_timing ());
-fun new_task pri = Task ((pri, new_id ()), new_timing ());
+val dummy_task = Task {name = "", id = ~1, pri = NONE, timing = new_timing ()};
+fun new_task name pri = Task {name = name, id = new_id (), pri = pri, timing = new_timing ()};
 
-fun pri_of_task (Task ((pri, _), _)) = the_default 0 pri;
-fun str_of_task (Task ((_, i), _)) = string_of_int i;
+fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
+fun str_of_task (Task {name, id, ...}) =
+  if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
 
-fun timing_of_task (Task (_, timing)) = Synchronized.value timing;
-fun running (Task (_, timing)) = gen_timing apfst timing;
-fun waiting (Task (_, timing)) = gen_timing apsnd timing;
+fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
+fun running (Task {timing, ...}) = gen_timing apfst timing;
+fun waiting (Task {timing, ...}) = gen_timing apsnd timing;
 
-fun task_ord (Task (t1, _), Task (t2, _)) =
-  prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
+fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
+  prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
 
 val eq_task = is_equal o task_ord;
 
@@ -219,15 +225,15 @@
 
 fun enqueue_passive group abort (Queue {groups, jobs}) =
   let
-    val task = new_task NONE;
+    val task = new_task "" NONE;
     val groups' = groups
       |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
     val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort));
   in (task, make_queue groups' jobs') end;
 
-fun enqueue group deps pri job (Queue {groups, jobs}) =
+fun enqueue name group deps pri job (Queue {groups, jobs}) =
   let
-    val task = new_task (SOME pri);
+    val task = new_task name (SOME pri);
     val groups' = groups
       |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
     val jobs' = jobs
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -663,13 +663,15 @@
 
         val future_proof = Proof.global_future_proof
           (fn prf =>
-            Future.fork_pri ~1 (fn () =>
-              let val (states, result_state) =
-                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
-                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                |> fold_map command_result body_trs
-                ||> command (end_tr |> set_print false);
-              in (states, presentation_context_of result_state) end))
+            singleton
+              (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
+              (fn () =>
+                let val (states, result_state) =
+                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
+                  |> fold_map command_result body_trs
+                  ||> command (end_tr |> set_print false);
+                in (states, presentation_context_of result_state) end))
           #> (fn (states, ctxt) => States.put (SOME states) ctxt);
 
         val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -208,7 +208,9 @@
 
 fun async_state tr st =
   ignore
-    (singleton (Future.bulk {group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
+    (singleton
+      (Future.bulk {name = "Document.async_state",
+        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
       (fn () =>
         Toplevel.setmp_thread_position tr
           (fn () => Toplevel.print_state false st) ()));
@@ -327,7 +329,7 @@
 (* execute *)
 
 fun execute version_id state =
-  state |> map_state (fn (versions, commands, execs, execution) =>
+  state |> map_state (fn (versions, commands, execs, _) =>
     let
       val version = the_version state version_id;
 
@@ -337,14 +339,15 @@
       val _ = cancel state;
 
       val execution' = (* FIXME proper node deps *)
-        Future.bulk {group = NONE, deps = [], pri = 1} [fn () =>
-          let
-            val _ = await_cancellation state;
-            val _ =
-              node_names_of version |> List.app (fn name =>
-                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
-                    (get_node version name) ());
-          in () end];
+        Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
+          [fn () =>
+            let
+              val _ = await_cancellation state;
+              val _ =
+                node_names_of version |> List.app (fn name =>
+                  fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+                      (get_node version name) ());
+            in () end];
 
       val _ = await_cancellation state;  (* FIXME async!? *)
 
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -182,15 +182,17 @@
           let
             val get = the o Symtab.lookup tab;
             val deps = map (`get) (Graph.imm_preds task_graph name);
+            val task_deps = map (Future.task_of o #1) deps;
             fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
 
             val future =
-              singleton (Future.bulk {group = NONE, deps = map (Future.task_of o #1) deps, pri = 0})
-              (fn () =>
-                (case map_filter failed deps of
-                  [] => body (map (#1 o Future.join o get) parents)
-                | bad => error (loader_msg
-                    ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+              singleton
+                (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
+                (fn () =>
+                  (case map_filter failed deps of
+                    [] => body (map (#1 o Future.join o get) parents)
+                  | bad => error (loader_msg ("failed to load " ^ quote name ^
+                      " (unresolved " ^ commas_quote bad ^ ")") [])));
           in Symtab.update (name, future) tab end
       | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
     val _ =
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/goal.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -106,7 +106,9 @@
 
 (* parallel proofs *)
 
-fun fork e = Future.fork_pri ~1 (fn () => Future.status e);
+fun fork e =
+  singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
+    (fn () => Future.status e);
 
 val parallel_proofs = Unsynchronized.ref 1;
 
diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jan 31 21:54:49 2011 +0100
+++ b/src/Pure/proofterm.ML	Mon Jan 31 22:57:01 2011 +0100
@@ -1390,7 +1390,7 @@
       else Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
       singleton
-        (Future.bulk {group = NONE,
+        (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
             deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1446,7 +1446,10 @@
     val body0 =
       if ! proofs <> 2 then Future.value (make_body0 MinProof)
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
-      else Future.fork_pri ~1 (make_body0 o full_proof0);
+      else
+        singleton
+          (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+          (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =