# 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;