60 (* groups *) |
60 (* groups *) |
61 |
61 |
62 abstype group = Group of |
62 abstype group = Group of |
63 {parent: group option, |
63 {parent: group option, |
64 id: int, |
64 id: int, |
65 status: exn option Synchronized.var} |
65 status: exn option Unsynchronized.ref} |
66 with |
66 with |
67 |
67 |
68 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; |
68 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; |
69 |
69 |
70 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE); |
70 fun new_group parent = |
|
71 make_group (parent, new_id (), Unsynchronized.ref NONE); |
71 |
72 |
72 fun group_id (Group {id, ...}) = id; |
73 fun group_id (Group {id, ...}) = id; |
73 fun eq_group (group1, group2) = group_id group1 = group_id group2; |
74 fun eq_group (group1, group2) = group_id group1 = group_id group2; |
74 |
75 |
75 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a |
76 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a |
76 | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a); |
77 | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a); |
77 |
78 |
78 |
79 |
79 (* group status *) |
80 (* group status *) |
80 |
81 |
|
82 local |
|
83 |
|
84 fun is_canceled_unsynchronized (Group {parent, status, ...}) = |
|
85 is_some (! status) orelse |
|
86 (case parent of NONE => false | SOME group => is_canceled_unsynchronized group); |
|
87 |
|
88 fun group_status_unsynchronized (Group {parent, status, ...}) = |
|
89 the_list (! status) @ |
|
90 (case parent of NONE => [] | SOME group => group_status_unsynchronized group); |
|
91 |
|
92 val lock = Mutex.mutex (); |
|
93 fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e; |
|
94 |
|
95 in |
|
96 |
81 fun cancel_group (Group {status, ...}) exn = |
97 fun cancel_group (Group {status, ...}) exn = |
82 Synchronized.change status |
98 SYNCHRONIZED (fn () => |
83 (fn exns => SOME (Par_Exn.make (exn :: the_list exns))); |
99 Unsynchronized.change status (fn exns => SOME (Par_Exn.make (exn :: the_list exns)))); |
84 |
100 |
85 fun is_canceled (Group {parent, status, ...}) = |
101 fun is_canceled group = |
86 is_some (Synchronized.value status) orelse |
102 SYNCHRONIZED (fn () => is_canceled_unsynchronized group); |
87 (case parent of NONE => false | SOME group => is_canceled group); |
103 |
88 |
104 fun group_status group = |
89 fun group_status (Group {parent, status, ...}) = |
105 SYNCHRONIZED (fn () => group_status_unsynchronized group); |
90 the_list (Synchronized.value status) @ |
106 |
91 (case parent of NONE => [] | SOME group => group_status group); |
107 end; |
92 |
108 |
93 fun str_of_group group = |
109 fun str_of_group group = |
94 (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); |
110 (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); |
95 |
111 |
96 fun str_of_groups group = |
112 fun str_of_groups group = |