clarified positions of theory imports;

--- a/src/Pure/Isar/token.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/Isar/token.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -182,7 +182,7 @@
       else new Pos(line1, offset1, file, id)
     }
 
-    def position(end_offset: Symbol.Offset): Position.T =
+    private def position(end_offset: Symbol.Offset): Position.T =
       (if (line > 0) Position.Line(line) else Nil) :::
       (if (offset > 0) Position.Offset(offset) else Nil) :::
       (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
@@ -204,7 +204,7 @@
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none)
+  def reader(tokens: List[Token], file: String, id: Document_ID.Generic = Document_ID.none)
     : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
 }
 

--- 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))

--- a/src/Pure/PIDE/protocol.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -433,7 +433,7 @@
           { case Document.Node.Deps(header) =>
               val master_dir = Isabelle_System.posix_path_url(name.master_dir)
               val theory = Long_Name.base_name(name.theory)
-              val imports = header.imports.map(_.node)
+              val imports = header.imports.map({ case (a, _) => a.node })
               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
                 pair(Encode.string, pair(Encode.string, pair(list(Encode.string),

--- a/src/Pure/PIDE/resources.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -91,7 +91,7 @@
   {
     if (reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader).decode_symbols
+        val header = Thy_Header.read(reader, node_name.node).decode_symbols
 
         val base_name = Long_Name.base_name(node_name.theory)
         val (name, pos) = header.name
@@ -100,7 +100,7 @@
             " for theory " + quote(name) + Position.here(pos))
 
         val imports =
-          header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) })
+          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
         Document.Node.Header(imports, header.keywords, Nil)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }

--- a/src/Pure/Thy/thy_header.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -124,7 +124,7 @@
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char]): Thy_Header =
+  def read(reader: Reader[Char], file: String): Thy_Header =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
     val toks = new mutable.ListBuffer[Token]
@@ -140,14 +140,14 @@
     }
     scan_to_begin(reader)
 
-    parse(commit(header), Token.reader(toks.toList)) match {
+    parse(commit(header), Token.reader(toks.toList, file)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
 
-  def read(source: CharSequence): Thy_Header =
-    read(new CharSequenceReader(source))
+  def read(source: CharSequence, file: String): Thy_Header =
+    read(new CharSequenceReader(source), file)
 }
 
 

--- a/src/Pure/Thy/thy_info.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/Thy/thy_info.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -106,7 +106,7 @@
           if (parent_loaded(dep.name.theory)) g
           else {
             val a = node(dep.name)
-            val bs = dep.header.imports.map(node _)
+            val bs = dep.header.imports.map({ case (name, _) => node(name) })
             ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
           }
       }
@@ -136,8 +136,7 @@
         val header =
           try { resources.check_thy(session, name).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
-        val imports = header.imports.map((_, Position.File(name.node)))
-        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
+        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
       }
       catch {
         case e: Throwable =>

--- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 18:18:40 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 19:51:36 2015 +0100
@@ -82,7 +82,7 @@
           node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
         if (update_header) {
           val node1 = node.update_header(header)
-          if (node.header.imports != node1.header.imports ||
+          if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
               node.header.keywords != node1.header.keywords) syntax_changed0 += name
           nodes += (name -> node1)
           doc_edits += (name -> Document.Node.Deps(header))
@@ -98,7 +98,7 @@
         if (node.is_empty) None
         else {
           val header = node.header
-          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
+          val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
           Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
         }
       nodes += (name -> node.update_syntax(syntax))