src/Pure/PIDE/document.ML
changeset 40520 77a7b0a7d4b1
parent 40481 da2c56aaaa68
child 40532 f51c478ef85a
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Nov 13 00:24:41 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Nov 13 11:41:02 2010 +0100
     1.3 @@ -319,8 +319,7 @@
     1.4          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
     1.5  
     1.6        val _ = List.app Future.cancel execution;
     1.7 -      fun await_cancellation () =
     1.8 -        uninterruptible (fn _ => fn () => Future.join_results execution) ();
     1.9 +      fun await_cancellation () = Future.join_results execution;
    1.10  
    1.11        val execution' = (* FIXME proper node deps *)
    1.12          node_names_of version |> map (fn name =>
    1.13 @@ -328,6 +327,9 @@
    1.14              (await_cancellation ();
    1.15                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.16                  (get_node version name) ())));
    1.17 +
    1.18 +      val _ = await_cancellation ();
    1.19 +
    1.20      in (versions, commands, execs, execution') end);
    1.21  
    1.22  end;