equal
deleted
inserted
replaced
114 |
114 |
115 fun count_forked i = |
115 fun count_forked i = |
116 Synchronized.change forked_proofs (fn (m, groups, tab) => |
116 Synchronized.change forked_proofs (fn (m, groups, tab) => |
117 let |
117 let |
118 val n = m + i; |
118 val n = m + i; |
119 val _ = |
119 val _ = Future.forked_proofs := n; |
120 Multithreading.tracing 2 (fn () => |
|
121 ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); |
|
122 in (n, groups, tab) end); |
120 in (n, groups, tab) end); |
123 |
121 |
124 fun register_forked id future = |
122 fun register_forked id future = |
125 Synchronized.change forked_proofs (fn (m, groups, tab) => |
123 Synchronized.change forked_proofs (fn (m, groups, tab) => |
126 let |
124 let |
174 fun peek_futures id = |
172 fun peek_futures id = |
175 Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; |
173 Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; |
176 |
174 |
177 fun reset_futures () = |
175 fun reset_futures () = |
178 Synchronized.change_result forked_proofs (fn (m, groups, tab) => |
176 Synchronized.change_result forked_proofs (fn (m, groups, tab) => |
179 (groups, (0, [], Inttab.empty))); |
177 (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty)))); |
180 |
178 |
181 end; |
179 end; |
182 |
180 |
183 |
181 |
184 (* scheduling parameters *) |
182 (* scheduling parameters *) |