# HG changeset patch
# User wenzelm
# Date 1289335925 -3600
# Node ID 8eab60e1baeba941415846bd0d8224b56560e361
# Parent  9c390868d2554507679019c87e78f0fa224af5e8
private counter, to keep externalized ids a bit smaller;

diff -r 9c390868d255 -r 8eab60e1baeb src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Nov 09 21:44:19 2010 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Nov 09 21:52:05 2010 +0100
@@ -38,13 +38,16 @@
 structure Task_Queue: TASK_QUEUE =
 struct
 
+val new_id = Synchronized.counter ();
+
+
 (* tasks *)
 
-abstype task = Task of int option * serial
+abstype task = Task of int option * int
 with
 
 val dummy_task = Task (NONE, ~1);
-fun new_task pri = Task (pri, serial ());
+fun new_task pri = Task (pri, new_id ());
 
 fun pri_of_task (Task (pri, _)) = the_default 0 pri;
 fun str_of_task (Task (_, i)) = string_of_int i;
@@ -61,13 +64,13 @@
 
 abstype group = Group of
  {parent: group option,
-  id: serial,
+  id: int,
   status: exn list Synchronized.var}
 with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
-fun new_group parent = make_group (parent, serial (), Synchronized.var "group" []);
+fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
 
 fun group_id (Group {id, ...}) = id;
 fun eq_group (group1, group2) = group_id group1 = group_id group2;