src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Fri Apr 20 20:29:44 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 20 22:51:06 2012 +0200
@@ -400,24 +400,26 @@
             NONE => true
           | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
       in (visible', initial') end;
-    fun get_common ((prev, id), opt_exec) (found, (_, flags)) =
-      if found then NONE
-      else
-        let val found' =
-          (case opt_exec of
-            NONE => true
-          | SOME (exec_id, exec) =>
-              (case lookup_entry node0 id of
-                NONE => true
-              | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec));
-        in SOME (found', (prev, update_flags prev flags)) end;
-    val (found, (common, flags)) =
-      iterate_entries get_common node (false, (NONE, (true, true)));
+    fun get_common ((prev, id), opt_exec) (same, (_, flags)) =
+      if same then
+        let
+          val flags' = update_flags prev flags;
+          val same' =
+            (case opt_exec of
+              NONE => false
+            | SOME (exec_id, exec) =>
+                (case lookup_entry node0 id of
+                  NONE => false
+                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec));
+        in SOME (same', (prev, flags')) end
+      else NONE;
+    val (same, (common, flags)) =
+      iterate_entries get_common node (true, (NONE, (true, true)));
   in
-    if found then (common, flags)
-    else
+    if same then
       let val last = Entries.get_after (get_entries node) common
       in (last, update_flags last flags) end
+    else (common, flags)
   end;
 
 fun illegal_init () = error "Illegal theory header after end of theory";