--- a/src/Pure/PIDE/document.ML Sat Nov 13 00:24:41 2010 +0100
+++ b/src/Pure/PIDE/document.ML Sat Nov 13 11:41:02 2010 +0100
@@ -319,8 +319,7 @@
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
val _ = List.app Future.cancel execution;
- fun await_cancellation () =
- uninterruptible (fn _ => fn () => Future.join_results execution) ();
+ fun await_cancellation () = Future.join_results execution;
val execution' = (* FIXME proper node deps *)
node_names_of version |> map (fn name =>
@@ -328,6 +327,9 @@
(await_cancellation ();
fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
(get_node version name) ())));
+
+ val _ = await_cancellation ();
+
in (versions, commands, execs, execution') end);
end;