# HG changeset patch
# User wenzelm
# Date 1228518131 -3600
# Node ID 23cbaa9f9834d2d8730f824605b4b306a66d6723
# Parent  1b99dcae2156b525bd927d3e11f19552b0e4bd45
added new_task;

diff -r 1b99dcae2156 -r 23cbaa9f9834 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 00:01:57 2008 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 00:02:11 2008 +0100
@@ -8,6 +8,7 @@
 signature TASK_QUEUE =
 sig
   eqtype task
+  val new_task: unit -> task
   val str_of_task: task -> string
   eqtype group
   val new_group: unit -> group
@@ -34,8 +35,11 @@
 (* identifiers *)
 
 datatype task = Task of serial;
+fun new_task () = Task (serial ());
+
 fun str_of_task (Task i) = string_of_int i;
 
+
 datatype group = Group of serial * bool ref;
 
 fun new_group () = Group (serial (), ref true);
@@ -81,8 +85,7 @@
 
 fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
   let
-    val id = serial ();
-    val task = Task id;
+    val task as Task id = new_task ();
     val groups' = Inttab.cons_list (gid, task) groups;
     val jobs' = jobs
       |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;