equal
deleted
inserted
replaced
15 val group_status: group -> exn list |
15 val group_status: group -> exn list |
16 val str_of_group: group -> string |
16 val str_of_group: group -> string |
17 val str_of_groups: group -> string |
17 val str_of_groups: group -> string |
18 type task |
18 type task |
19 val dummy_task: task |
19 val dummy_task: task |
20 val new_task: group -> string -> int option -> task |
|
21 val group_of_task: task -> group |
20 val group_of_task: task -> group |
22 val name_of_task: task -> string |
21 val name_of_task: task -> string |
23 val pri_of_task: task -> int |
22 val pri_of_task: task -> int |
24 val str_of_task: task -> string |
23 val str_of_task: task -> string |
25 val str_of_task_groups: task -> string |
24 val str_of_task_groups: task -> string |
34 val all_passive: queue -> bool |
33 val all_passive: queue -> bool |
35 val status: queue -> {ready: int, pending: int, running: int, passive: int} |
34 val status: queue -> {ready: int, pending: int, running: int, passive: int} |
36 val cancel: queue -> group -> Thread.thread list |
35 val cancel: queue -> group -> Thread.thread list |
37 val cancel_all: queue -> group list * Thread.thread list |
36 val cancel_all: queue -> group list * Thread.thread list |
38 val finish: task -> queue -> bool * queue |
37 val finish: task -> queue -> bool * queue |
|
38 val enroll: Thread.thread -> string -> group -> queue -> task * queue |
39 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue |
39 val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue |
40 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
40 val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue |
41 val extend: task -> (bool -> bool) -> queue -> queue option |
41 val extend: task -> (bool -> bool) -> queue -> queue option |
42 val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue |
42 val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue |
43 val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue |
43 val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue |
293 val jobs' = Task_Graph.del_node task jobs; |
293 val jobs' = Task_Graph.del_node task jobs; |
294 val maximal = Task_Graph.is_maximal jobs task; |
294 val maximal = Task_Graph.is_maximal jobs task; |
295 in (maximal, make_queue groups' jobs') end; |
295 in (maximal, make_queue groups' jobs') end; |
296 |
296 |
297 |
297 |
|
298 (* enroll *) |
|
299 |
|
300 fun enroll thread name group (Queue {groups, jobs}) = |
|
301 let |
|
302 val task = new_task group name NONE; |
|
303 val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; |
|
304 val jobs' = jobs |> Task_Graph.new_node (task, Running thread); |
|
305 in (task, make_queue groups' jobs') end; |
|
306 |
|
307 |
298 (* enqueue *) |
308 (* enqueue *) |
299 |
309 |
300 fun enqueue_passive group abort (Queue {groups, jobs}) = |
310 fun enqueue_passive group abort (Queue {groups, jobs}) = |
301 let |
311 let |
302 val task = new_task group "passive" NONE; |
312 val task = new_task group "passive" NONE; |