tuned signature;

--- a/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 12:16:58 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 12:24:27 2009 +0200
@@ -11,27 +11,27 @@
   val pri_of_task: task -> int
   val str_of_task: task -> string
   type group
+  val new_group: group option -> group
   val group_id: group -> int
   val eq_group: group * group -> bool
-  val new_group: group option -> group
+  val cancel_group: group -> exn -> unit
+  val is_canceled: group -> bool
   val group_status: group -> exn list
   val str_of_group: group -> string
   type queue
   val empty: queue
   val is_empty: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int}
+  val cancel: queue -> group -> bool
+  val cancel_all: queue -> group list
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
   val dequeue_towards: task list -> queue ->
     (((task * group * (bool -> bool) list) * task list) option * queue)
+  val finish: task -> queue -> bool * queue
   val interrupt: queue -> task -> unit
   val interrupt_external: queue -> string -> unit
-  val is_canceled: group -> bool
-  val cancel_group: group -> exn -> unit
-  val cancel: queue -> group -> bool
-  val cancel_all: queue -> group list
-  val finish: task -> queue -> bool * queue
 end;
 
 structure Task_Queue:> TASK_QUEUE =
@@ -67,17 +67,19 @@
   id :: (case parent of NONE => [] | SOME group => group_ancestry group);
 
 
+(* group status *)
+
 fun cancel_group (Group {status, ...}) exn = CRITICAL (fn () =>
   (case exn of
     Exn.Interrupt => if null (! status) then status := [exn] else ()
   | _ => change status (cons exn)));
 
+fun is_canceled (Group {parent, status, ...}) = (*non-critical*)
+  not (null (! status)) orelse (case parent of NONE => false | SOME group => is_canceled group);
+
 fun group_status (Group {parent, status, ...}) = (*non-critical*)
   ! status @ (case parent of NONE => [] | SOME group => group_status group);
 
-fun is_canceled (Group {parent, status, ...}) = (*non-critical*)
-  not (null (! status)) orelse (case parent of NONE => false | SOME group => is_canceled group);
-
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
 
@@ -226,6 +228,19 @@
   end;
 
 
+(* finish *)
+
+fun finish task (Queue {groups, jobs, cache}) =
+  let
+    val group = get_group jobs task;
+    val groups' = groups
+      |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
+    val jobs' = Task_Graph.del_node task jobs;
+    val maximal = null (Task_Graph.imm_succs jobs task);
+    val cache' = if maximal then cache else Unknown;
+  in (maximal, make_queue groups' jobs' cache') end;
+
+
 (* sporadic interrupts *)
 
 fun interrupt (Queue {jobs, ...}) task =
@@ -241,17 +256,4 @@
         of SOME task => interrupt queue task | NONE => ())
   | NONE => ());
 
-
-(* termination *)
-
-fun finish task (Queue {groups, jobs, cache}) =
-  let
-    val group = get_group jobs task;
-    val groups' = groups
-      |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
-    val jobs' = Task_Graph.del_node task jobs;
-    val maximal = null (Task_Graph.imm_succs jobs task);
-    val cache' = if maximal then cache else Unknown;
-  in (maximal, make_queue groups' jobs' cache') end;
-
 end;