clarified active_job: take dependencies into account (e.g. future based on promise);
authorwenzelm
Fri, 09 Jan 2015 21:20:07 +0100
changeset 59333 4ef80efc36c8
parent 59332 56fec2b5b826
child 59334 f0141b991c8f
clarified active_job: take dependencies into account (e.g. future based on promise);
src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Jan 09 20:51:26 2015 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Jan 09 21:20:07 2015 +0100
@@ -233,10 +233,8 @@
       else NONE
   | ready_job _ = NONE;
 
-fun active_job (_, (Job _, _)) = SOME ()
-  | active_job (_, (Running _, _)) = SOME ()
-  | active_job (task, (Passive _, _)) =
-      if is_canceled (group_of_task task) then SOME () else NONE;
+fun active_job (task, (Running _, _)) = SOME (task, [])
+  | active_job arg = ready_job arg;
 
 fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs);