35 val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int} |
35 val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int} |
36 val cancel: queue -> group -> Thread.thread list |
36 val cancel: queue -> group -> Thread.thread list |
37 val cancel_all: queue -> group list * Thread.thread list |
37 val cancel_all: queue -> group list * Thread.thread list |
38 val finish: task -> queue -> bool * queue |
38 val finish: task -> queue -> bool * queue |
39 val enroll: Thread.thread -> string -> group -> queue -> task * queue |
39 val enroll: Thread.thread -> string -> group -> queue -> task * queue |
40 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue |
40 val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue |
41 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
41 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
42 val extend: task -> (bool -> bool) -> queue -> queue option |
42 val extend: task -> (bool -> bool) -> queue -> queue option |
43 val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue |
43 val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue |
44 val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue |
44 val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue |
45 val dequeue_deps: Thread.thread -> task list -> queue -> |
45 val dequeue_deps: Thread.thread -> task list -> queue -> |
310 in (task, make_queue groups' jobs' urgent) end; |
310 in (task, make_queue groups' jobs' urgent) end; |
311 |
311 |
312 |
312 |
313 (* enqueue *) |
313 (* enqueue *) |
314 |
314 |
315 fun enqueue_passive group abort (Queue {groups, jobs, urgent}) = |
315 fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) = |
316 let |
316 let |
317 val task = new_task group "passive" NONE; |
317 val task = new_task group name NONE; |
318 val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; |
318 val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; |
319 val jobs' = jobs |> Task_Graph.new_node (task, Passive abort); |
319 val jobs' = jobs |> Task_Graph.new_node (task, Passive abort); |
320 in (task, make_queue groups' jobs' urgent) end; |
320 in (task, make_queue groups' jobs' urgent) end; |
321 |
321 |
322 fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) = |
322 fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) = |