# HG changeset patch
# User wenzelm
# Date 1334954928 -7200
# Node ID 97d28302445cf99e88336a37d504c519308daf73
# Parent  8d654975b67df39ccadc6c22127a87eb2e56aa4a
always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

diff -r 8d654975b67d -r 97d28302445c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Apr 20 22:51:06 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 20 22:48:48 2012 +0200
@@ -472,7 +472,7 @@
                 val required = is_required name;
               in
                 if updated_imports orelse AList.defined (op =) edits name orelse
-                  required andalso not (stable_finished_theory node)
+                  not (stable_finished_theory node)
                 then
                   let
                     val node0 = node_of old_version name;