clarified span position;

--- a/src/Pure/Isar/token.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Isar/token.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -158,7 +158,9 @@
   object Pos
   {
     val none: Pos = new Pos(0, 0, "")
-    def file(file: String): Pos = new Pos(0, 0, file)
+    val start: Pos = new Pos(1, 1, "")
+    val offset: Pos = new Pos(0, 1, "")
+    def file(file: String): Pos = new Pos(1, 1, file)
   }
 
   final class Pos private[Token](
@@ -203,8 +205,8 @@
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token], file: String): Reader =
-    new Token_Reader(tokens, Pos.file(file))
+  def reader(tokens: List[Token], start: Token.Pos): Reader =
+    new Token_Reader(tokens, start)
 }
 
 

--- a/src/Pure/PIDE/command.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -10,6 +10,7 @@
 
 import scala.collection.mutable
 import scala.collection.immutable.SortedMap
+import scala.util.parsing.input.CharSequenceReader
 
 
 object Command
@@ -354,12 +355,14 @@
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
-    header: Document.Node.Header,
     span: Command_Span.Span): Blobs_Info =
   {
     span.kind match {
       // inlined errors
       case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
+        val header =
+          resources.check_thy_reader("", node_name,
+            new CharSequenceReader(span.source), Token.Pos.offset)
         val import_errors =
           for ((imp, pos) <- header.imports if !can_import(imp))
             yield "Bad theory import " + quote(imp.node) + Position.here(pos)

--- a/src/Pure/PIDE/command_span.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -28,23 +28,24 @@
   {
     def length: Int = (0 /: content)(_ + _.source.length)
 
+    def source: String =
+      content match {
+        case List(tok) => tok.source
+        case toks => toks.map(_.source).mkString
+      }
+
     def compact_source: (String, Span) =
     {
-      val source: String =
-        content match {
-          case List(tok) => tok.source
-          case toks => toks.map(_.source).mkString
-        }
-
+      val src = source
       val content1 = new mutable.ListBuffer[Token]
       var i = 0
       for (Token(kind, s) <- content) {
         val n = s.length
-        val s1 = source.substring(i, i + n)
+        val s1 = src.substring(i, i + n)
         content1 += Token(kind, s1)
         i += n
       }
-      (source, Span(kind, content1.toList))
+      (src, Span(kind, content1.toList))
     }
   }
 

--- a/src/Pure/PIDE/resources.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -86,12 +86,12 @@
     }
   }
 
-  def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char])
-    : Document.Node.Header =
+  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
+    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
   {
     if (reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader, node_name.node).decode_symbols
+        val header = Thy_Header.read(reader, start).decode_symbols
 
         val base_name = Long_Name.base_name(node_name.theory)
         val (name, pos) = header.name
@@ -108,8 +108,9 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(qualifier, name, _))
+  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
+    : Document.Node.Header =
+    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
 
   def check_file(file: String): Boolean =
     try {

--- a/src/Pure/System/options.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/System/options.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -110,7 +110,7 @@
     {
       val toks = Token.explode(syntax.keywords, File.read(file))
       val ops =
-        parse_all(rep(parser), Token.reader(toks, file.implode)) match {
+        parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
           case Success(result, _) => result
           case bad => error(bad.toString)
         }

--- a/src/Pure/Thy/thy_header.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -124,7 +124,7 @@
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char], file: String): Thy_Header =
+  def read(reader: Reader[Char], start: Token.Pos): 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, file)) match {
+    parse(commit(header), Token.reader(toks.toList, start)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
 
-  def read(source: CharSequence, file: String): Thy_Header =
-    read(new CharSequenceReader(source), file)
+  def read(source: CharSequence, start: Token.Pos): Thy_Header =
+    read(new CharSequenceReader(source), start)
 }
 
 

--- a/src/Pure/Thy/thy_info.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Thy/thy_info.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -134,7 +134,7 @@
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { resources.check_thy(session, name).cat_errors(message) }
+          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
         Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
       }

--- a/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -159,15 +159,13 @@
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
-    header: Document.Node.Header,
     commands: Linear_Set[Command],
     first: Command, last: Command): Linear_Set[Command] =
   {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
       syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
-        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, header, span),
-          span))
+        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, span), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
 
@@ -213,7 +211,6 @@
     // FIXME somewhat slow
     def recover_spans(
       name: Document.Node.Name,
-      header: Document.Node.Header,
       perspective: Command.Perspective,
       commands: Linear_Set[Command]): Linear_Set[Command] =
     {
@@ -229,7 +226,7 @@
             val first = next_invisible(cmds.reverse, first_unparsed)
             val last = next_invisible(cmds, first_unparsed)
             recover(
-              reparse_spans(resources, syntax, get_blob, can_import, name, header, cmds, first, last))
+              reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
           case None => cmds
         }
       recover(commands)
@@ -244,7 +241,7 @@
         if (name.is_theory) {
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
-          val commands2 = recover_spans(name, node.header, node.perspective.visible, commands1)
+          val commands2 = recover_spans(name, node.perspective.visible, commands1)
           node.update_commands(commands2)
         }
         else node
@@ -274,8 +271,8 @@
                         last = it.next
                         i += last.length
                       }
-                      reparse_spans(resources, syntax, get_blob, can_import, name,
-                        node.header, commands, first_unfinished, last)
+                      reparse_spans(resources, syntax, get_blob, can_import,
+                        name, commands, first_unfinished, last)
                     case None => commands
                   }
                 case None => commands
@@ -330,7 +327,7 @@
               if (reparse_set(name) && commands.nonEmpty)
                 node.update_commands(
                   reparse_spans(resources, syntax, get_blob, can_import, name,
-                    node.header, commands, commands.head, commands.last))
+                    commands, commands.head, commands.last))
               else node
             val node2 =
               (node1 /: edits)(

--- a/src/Pure/Tools/build.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Tools/build.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -260,8 +260,9 @@
     def parse_entries(root: Path): List[(String, Session_Entry)] =
     {
       val toks = Token.explode(root_syntax.keywords, File.read(root))
+      val start = Token.Pos.file(root.implode)
 
-      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
+      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
         case Success(result, _) =>
           var chapter = chapter_default
           val entries = new mutable.ListBuffer[(String, Session_Entry)]

--- a/src/Tools/jEdit/src/document_model.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -79,7 +79,8 @@
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
         Exn.capture {
-          PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
+          PIDE.resources.check_thy_reader("", node_name,
+            JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
         } match {
           case Exn.Res(header) => header
           case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))