equal
deleted
inserted
replaced
36 val cancel_all: queue -> group list * Thread.thread list |
36 val cancel_all: queue -> group list * Thread.thread list |
37 val finish: task -> queue -> bool * queue |
37 val finish: task -> queue -> bool * queue |
38 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue |
38 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue |
39 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
39 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
40 val extend: task -> (bool -> bool) -> queue -> queue option |
40 val extend: task -> (bool -> bool) -> queue -> queue option |
41 val dequeue_passive: Thread.thread -> task -> queue -> bool * queue |
41 val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue |
42 val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue |
42 val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue |
43 val dequeue_deps: Thread.thread -> task list -> queue -> |
43 val dequeue_deps: Thread.thread -> task list -> queue -> |
44 (((task * (bool -> bool) list) option * task list) * queue) |
44 (((task * (bool -> bool) list) option * task list) * queue) |
45 end; |
45 end; |
46 |
46 |
315 |
315 |
316 fun dequeue_passive thread task (queue as Queue {groups, jobs}) = |
316 fun dequeue_passive thread task (queue as Queue {groups, jobs}) = |
317 (case try (get_job jobs) task of |
317 (case try (get_job jobs) task of |
318 SOME (Passive _) => |
318 SOME (Passive _) => |
319 let val jobs' = set_job task (Running thread) jobs |
319 let val jobs' = set_job task (Running thread) jobs |
320 in (true, make_queue groups jobs') end |
320 in (SOME true, make_queue groups jobs') end |
321 | _ => (false, queue)); |
321 | SOME _ => (SOME false, queue) |
|
322 | NONE => (NONE, queue)); |
322 |
323 |
323 fun dequeue thread (queue as Queue {groups, jobs}) = |
324 fun dequeue thread (queue as Queue {groups, jobs}) = |
324 (case Task_Graph.get_first (uncurry ready_job) jobs of |
325 (case Task_Graph.get_first (uncurry ready_job) jobs of |
325 SOME (result as (task, _)) => |
326 SOME (result as (task, _)) => |
326 let val jobs' = set_job task (Running thread) jobs |
327 let val jobs' = set_job task (Running thread) jobs |