# HG changeset patch
# User wenzelm
# Date 1289644862 -3600
# Node ID 77a7b0a7d4b1d3cd747d0532cb27ca98bbd3c045
# Parent  d02e483ee82ab504e44d760cf77a9eb17131f1ff
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

diff -r d02e483ee82a -r 77a7b0a7d4b1 src/Pure/PIDE/document.ML
--- 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;