diff -r e0169f13bd37 -r fd81d51460b7 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Jul 29 18:59:58 2013 +0200 +++ b/src/Pure/PIDE/document.ML Mon Jul 29 19:55:38 2013 +0200 @@ -362,7 +362,7 @@ Symtab.fold (fn (a, ()) => exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? Symtab.update (a, ())) all_visible Symtab.empty; - in Symtab.defined required end; + in required end; fun init_theory deps node span = let @@ -459,7 +459,8 @@ val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); val nodes = nodes_of new_version; - val is_required = make_required nodes; + val required = make_required nodes; + val required0 = make_required (nodes_of old_version); val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty; val updated = timeit "Document.update" (fn () => @@ -472,9 +473,10 @@ let val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; - val node_required = is_required name; + val node_required = Symtab.defined required name; in - if Symtab.defined edited name orelse visible_node node orelse imports_result_changed + if Symtab.defined edited name orelse visible_node node orelse + imports_result_changed orelse Symtab.defined required0 name <> node_required then let val node0 = node_of old_version name;