always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
--- 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;