1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 31 22:34:37 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 01 19:27:28 2012 +0200
     1.3 @@ -359,10 +359,13 @@
     1.4      |> Toplevel.end_theory Position.none
     1.5      |> Thm.join_theory_proofs) ()));
     1.6  
     1.7 -fun stable_command exec =
     1.8 +fun stable_exec_id id =
     1.9 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures id)));
    1.10 +
    1.11 +fun stable_exec exec =
    1.12    (case Exn.capture Command.memo_result exec of
    1.13      Exn.Exn exn => not (Exn.is_interrupt exn)
    1.14 -  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
    1.15 +  | Exn.Res _ => true);
    1.16  
    1.17  fun make_required nodes =
    1.18    let
    1.19 @@ -423,7 +426,8 @@
    1.20              | SOME (exec_id, exec) =>
    1.21                  (case lookup_entry node0 id of
    1.22                    NONE => false
    1.23 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec));
    1.24 +                | SOME (exec_id0, _) =>
    1.25 +                    exec_id = exec_id0 andalso stable_exec_id exec_id andalso stable_exec exec));
    1.26          in SOME (same', (prev, flags')) end
    1.27        else NONE;
    1.28      val (same, (common, flags)) =