# HG changeset patch
# User wenzelm
# Date 1229383187 -3600
# Node ID 5a79ec2fedfbf29fdee8746df926dc49c6b39895
# Parent  d9e423b9e7074368d97aa22c6ac061b4b2545ded
tuned enqueue: plain add_edge, acyclic not required here;

diff -r d9e423b9e707 -r 5a79ec2fedfb src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Dec 15 22:07:30 2008 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Dec 16 00:19:47 2008 +0100
@@ -62,6 +62,9 @@
 fun map_job (Task id) f (jobs: jobs) = IntGraph.map_node id (apsnd f) jobs;
 
 fun add_job (Task id) (Task dep) (jobs: jobs) =
+  IntGraph.add_edge (dep, id) jobs handle IntGraph.UNDEF _ => jobs;
+
+fun add_job_acyclic (Task id) (Task dep) (jobs: jobs) =
   IntGraph.add_edge_acyclic (dep, id) jobs handle IntGraph.UNDEF _ => jobs;
 
 fun check_job (jobs: jobs) (task as Task id) =
@@ -92,7 +95,7 @@
   in (task, make_queue groups' jobs' focus) end;
 
 fun depend deps task (Queue {groups, jobs, focus}) =
-  make_queue groups (fold (add_job task) deps jobs) focus;
+  make_queue groups (fold (add_job_acyclic task) deps jobs) focus;
 
 fun focus tasks (Queue {groups, jobs, ...}) =
   make_queue groups jobs (map_filter (check_job jobs) tasks);