equal
deleted
inserted
replaced
261 |
261 |
262 fun force_exec NONE = () |
262 fun force_exec NONE = () |
263 | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); |
263 | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); |
264 |
264 |
265 val _ = List.app Future.cancel execution; |
265 val _ = List.app Future.cancel execution; |
266 fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution; |
266 fun await_cancellation () = |
|
267 uninterruptible (fn _ => fn () => Future.join_results execution) (); |
267 |
268 |
268 val execution' = (* FIXME proper node deps *) |
269 val execution' = (* FIXME proper node deps *) |
269 node_names_of version |> map (fn name => |
270 node_names_of version |> map (fn name => |
270 Future.fork_pri 1 (fn () => |
271 Future.fork_pri 1 (fn () => |
271 (await_cancellation (); |
272 (await_cancellation (); |