src/Pure/PIDE/document.ML
changeset 52776 fd81d51460b7
parent 52775 e0169f13bd37
child 52784 4ba2e8b9972f
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 18:59:58 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 19:55:38 2013 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4        Symtab.fold (fn (a, ()) =>
     1.5          exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
     1.6            Symtab.update (a, ())) all_visible Symtab.empty;
     1.7 -  in Symtab.defined required end;
     1.8 +  in required end;
     1.9  
    1.10  fun init_theory deps node span =
    1.11    let
    1.12 @@ -459,7 +459,8 @@
    1.13      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
    1.14  
    1.15      val nodes = nodes_of new_version;
    1.16 -    val is_required = make_required nodes;
    1.17 +    val required = make_required nodes;
    1.18 +    val required0 = make_required (nodes_of old_version);
    1.19      val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
    1.20  
    1.21      val updated = timeit "Document.update" (fn () =>
    1.22 @@ -472,9 +473,10 @@
    1.23                let
    1.24                  val imports = map (apsnd Future.join) deps;
    1.25                  val imports_result_changed = exists (#4 o #1 o #2) imports;
    1.26 -                val node_required = is_required name;
    1.27 +                val node_required = Symtab.defined required name;
    1.28                in
    1.29 -                if Symtab.defined edited name orelse visible_node node orelse imports_result_changed
    1.30 +                if Symtab.defined edited name orelse visible_node node orelse
    1.31 +                  imports_result_changed orelse Symtab.defined required0 name <> node_required
    1.32                  then
    1.33                    let
    1.34                      val node0 = node_of old_version name;