src/Pure/PIDE/document.ML
changeset 46739 6024353549ca
parent 45674 eb65c9d17e2f
child 46876 8f3bb485f628
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Feb 29 23:31:35 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 01 11:28:33 2012 +0100
     1.3 @@ -212,15 +212,15 @@
     1.4          |> touch_node name
     1.5      | Header header =>
     1.6          let
     1.7 -          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
     1.8 +          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
     1.9            val nodes1 = nodes
    1.10              |> default_node name
    1.11 -            |> fold default_node parents;
    1.12 +            |> fold default_node imports;
    1.13            val nodes2 = nodes1
    1.14              |> Graph.Keys.fold
    1.15                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.16            val (header', nodes3) =
    1.17 -            (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.18 +            (header, Graph.add_deps_acyclic (name, imports) nodes2)
    1.19                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.20          in Graph.map_node name (set_header header') nodes3 end
    1.21          |> touch_node name