# HG changeset patch
# User wenzelm
# Date 1266614726 -3600
# Node ID 1c80c29086d74ad1e3c0f71f30f743fa6c676f1b
# Parent  3aea183d05dbf3727f2de5b126c1899534aa28db
eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;

diff -r 3aea183d05db -r 1c80c29086d7 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Feb 19 22:06:52 2010 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Feb 19 22:25:26 2010 +0100
@@ -34,12 +34,14 @@
   val finish: task -> queue -> bool * queue
 end;
 
-structure Task_Queue:> TASK_QUEUE =
+structure Task_Queue: TASK_QUEUE =
 struct
 
 (* tasks *)
 
-datatype task = Task of int option * serial;
+abstype task = Task of int option * serial
+with
+
 val dummy_task = Task (NONE, ~1);
 fun new_task pri = Task (pri, serial ());
 
@@ -47,15 +49,20 @@
 fun str_of_task (Task (_, i)) = string_of_int i;
 
 fun task_ord (Task t1, Task t2) = prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
+val eq_task = is_equal o task_ord;
+
+end;
+
 structure Task_Graph = Graph(type key = task val ord = task_ord);
 
 
 (* nested groups *)
 
-datatype group = Group of
+abstype group = Group of
  {parent: group option,
   id: serial,
-  status: exn list Synchronized.var};
+  status: exn list Synchronized.var}
+with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
@@ -90,6 +97,8 @@
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
 
+end;
+
 
 (* jobs *)
 
@@ -246,7 +255,7 @@
   let
     val group = get_group jobs task;
     val groups' = groups
-      |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
+      |> fold (fn gid => Inttab.remove_list eq_task (gid, task)) (group_ancestry group);
     val jobs' = Task_Graph.del_node task jobs;
     val maximal = null (Task_Graph.imm_succs jobs task);
   in (maximal, make_queue groups' jobs') end;