src/Pure/PIDE/document.scala
changeset 46739 6024353549ca
parent 46737 09ab89658a5d
child 46814 d68ea01d5084
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Feb 29 23:31:35 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 01 11:28:33 2012 +0100
     1.3 @@ -188,15 +188,15 @@
     1.4      def + (entry: (Node.Name, Node)): Nodes =
     1.5      {
     1.6        val (name, node) = entry
     1.7 -      val parents =
     1.8 +      val imports =
     1.9          node.header match {
    1.10 -          case Exn.Res(deps) => deps.imports.filter(_.dir != "")  // FIXME more specific filter
    1.11 +          case Exn.Res(deps) => deps.imports
    1.12            case _ => Nil
    1.13          }
    1.14        val graph1 =
    1.15 -        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
    1.16 +        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    1.17        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    1.18 -      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
    1.19 +      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
    1.20        new Nodes(graph3.map_node(name, _ => node))
    1.21      }
    1.22