10 val new_group: group option -> group |
10 val new_group: group option -> group |
11 val group_id: group -> int |
11 val group_id: group -> int |
12 val eq_group: group * group -> bool |
12 val eq_group: group * group -> bool |
13 val cancel_group: group -> exn -> unit |
13 val cancel_group: group -> exn -> unit |
14 val is_canceled: group -> bool |
14 val is_canceled: group -> bool |
15 val group_status: group -> exn list |
15 val group_status: group -> exn option |
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: unit -> task |
19 val dummy_task: unit -> task |
20 val group_of_task: task -> group |
20 val group_of_task: task -> group |
54 (* groups *) |
54 (* groups *) |
55 |
55 |
56 abstype group = Group of |
56 abstype group = Group of |
57 {parent: group option, |
57 {parent: group option, |
58 id: int, |
58 id: int, |
59 status: exn list Synchronized.var} |
59 status: exn option Synchronized.var} |
60 with |
60 with |
61 |
61 |
62 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; |
62 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; |
63 |
63 |
64 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []); |
64 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE); |
65 |
65 |
66 fun group_id (Group {id, ...}) = id; |
66 fun group_id (Group {id, ...}) = id; |
67 fun eq_group (group1, group2) = group_id group1 = group_id group2; |
67 fun eq_group (group1, group2) = group_id group1 = group_id group2; |
68 |
68 |
69 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a |
69 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a |
72 |
72 |
73 (* group status *) |
73 (* group status *) |
74 |
74 |
75 fun cancel_group (Group {status, ...}) exn = |
75 fun cancel_group (Group {status, ...}) exn = |
76 Synchronized.change status |
76 Synchronized.change status |
77 (fn exns => |
77 (fn exns => SOME (Par_Exn.make (exn :: the_list exns))); |
78 if not (Exn.is_interrupt exn) orelse null exns then exn :: exns |
|
79 else exns); |
|
80 |
78 |
81 fun is_canceled (Group {parent, status, ...}) = |
79 fun is_canceled (Group {parent, status, ...}) = |
82 not (null (Synchronized.value status)) orelse |
80 is_some (Synchronized.value status) orelse |
83 (case parent of NONE => false | SOME group => is_canceled group); |
81 (case parent of NONE => false | SOME group => is_canceled group); |
84 |
82 |
85 fun group_status (Group {parent, status, ...}) = |
83 fun group_exns (Group {parent, status, ...}) = |
86 Synchronized.value status @ |
84 the_list (Synchronized.value status) @ |
87 (case parent of NONE => [] | SOME group => group_status group); |
85 (case parent of NONE => [] | SOME group => group_exns group); |
|
86 |
|
87 fun group_status group = |
|
88 (case group_exns group of |
|
89 [] => NONE |
|
90 | exns => SOME (Par_Exn.make exns)); |
88 |
91 |
89 fun str_of_group group = |
92 fun str_of_group group = |
90 (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); |
93 (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); |
91 |
94 |
92 fun str_of_groups group = |
95 fun str_of_groups group = |