1.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 00:01:57 2008 +0100
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 00:02:11 2008 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  signature TASK_QUEUE =
     1.5  sig
     1.6    eqtype task
     1.7 +  val new_task: unit -> task
     1.8    val str_of_task: task -> string
     1.9    eqtype group
    1.10    val new_group: unit -> group
    1.11 @@ -34,8 +35,11 @@
    1.12  (* identifiers *)
    1.13  
    1.14  datatype task = Task of serial;
    1.15 +fun new_task () = Task (serial ());
    1.16 +
    1.17  fun str_of_task (Task i) = string_of_int i;
    1.18  
    1.19 +
    1.20  datatype group = Group of serial * bool ref;
    1.21  
    1.22  fun new_group () = Group (serial (), ref true);
    1.23 @@ -81,8 +85,7 @@
    1.24  
    1.25  fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
    1.26    let
    1.27 -    val id = serial ();
    1.28 -    val task = Task id;
    1.29 +    val task as Task id = new_task ();
    1.30      val groups' = Inttab.cons_list (gid, task) groups;
    1.31      val jobs' = jobs
    1.32        |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;