src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -81,7 +81,7 @@
     /* header and name */
 
     sealed case class Header(
-      imports: List[Name],
+      imports: List[(Name, Position.T)],
       keywords: Thy_Header.Keywords,
       errors: List[String])
     {
@@ -323,7 +323,7 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val imports = node.header.imports
+      val imports = node.header.imports.map(_._1)
       val graph1 =
         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))