src/Pure/PIDE/document.ML
changeset 49061 7449b804073b
parent 49012 8686c36fa27d
child 49064 bd6cc0b911a1
--- a/src/Pure/PIDE/document.ML	Fri Aug 31 22:34:37 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Sep 01 19:27:28 2012 +0200
@@ -359,10 +359,13 @@
     |> Toplevel.end_theory Position.none
     |> Thm.join_theory_proofs) ()));
 
-fun stable_command exec =
+fun stable_exec_id id =
+  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures id)));
+
+fun stable_exec exec =
   (case Exn.capture Command.memo_result exec of
     Exn.Exn exn => not (Exn.is_interrupt exn)
-  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
+  | Exn.Res _ => true);
 
 fun make_required nodes =
   let
@@ -423,7 +426,8 @@
             | SOME (exec_id, exec) =>
                 (case lookup_entry node0 id of
                   NONE => false
-                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec));
+                | SOME (exec_id0, _) =>
+                    exec_id = exec_id0 andalso stable_exec_id exec_id andalso stable_exec exec));
         in SOME (same', (prev, flags')) end
       else NONE;
     val (same, (common, flags)) =