# HG changeset patch
# User wenzelm
# Date 1222532288 -7200
# Node ID 70abca69247be3d7455b87fe25ff15b0774e8a01
# Parent  3c5b4f636159ab06a3f0a9010fd3892cb96e9087
dequeue_towards: return bound for unfinished tasks;

diff -r 3c5b4f636159 -r 70abca69247b src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Sep 27 18:18:07 2008 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Sep 27 18:18:08 2008 +0200
@@ -19,7 +19,8 @@
   val depend: task list -> task -> queue -> queue
   val focus: task list -> queue -> queue
   val dequeue: queue -> (task * group * (unit -> bool)) option * queue
-  val dequeue_towards: task list -> queue -> (task * group * (unit -> bool)) option * queue
+  val dequeue_towards: task list -> queue ->
+    (((task * group * (unit -> bool)) * task list) option * queue)
   val interrupt: queue -> task -> unit
   val interrupt_external: queue -> string -> unit
   val finish: task -> queue -> queue
@@ -126,7 +127,11 @@
   | res => res);
 
 fun dequeue_towards tasks (queue as Queue {jobs, ...}) =
-  dequeue_local (map_filter (check_job jobs) tasks) queue;
+  let val tasks' = map_filter (check_job jobs) tasks in
+    (case dequeue_local tasks' queue of
+      (NONE, queue') => (NONE, queue')
+    | (SOME work, queue') => (SOME (work, tasks'), queue'))
+  end;
 
 end;