more precise token positions;

--- a/src/Pure/General/position.scala	Tue Apr 08 12:31:17 2014 +0200
+++ b/src/Pure/General/position.scala	Tue Apr 08 13:24:08 2014 +0200
@@ -30,6 +30,10 @@
 
   object Line_File
   {
+    def apply(line: Int, file: String): T =
+      (if (line > 0) Line(line) else Nil) :::
+      (if (file != "") File(file) else Nil)
+
     def unapply(pos: T): Option[(Int, String)] =
       (pos, pos) match {
         case (Line(i), File(name)) => Some((i, name))

--- a/src/Pure/Isar/parse.scala	Tue Apr 08 12:31:17 2014 +0200
+++ b/src/Pure/Isar/parse.scala	Tue Apr 08 13:24:08 2014 +0200
@@ -25,31 +25,37 @@
       if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
-    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
-    {
-      def apply(raw_input: Input) =
-      {
-        val in = proper(raw_input)
-        if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
-        else {
-          val token = in.first
-          if (pred(token)) Success(token, proper(in.rest))
-          else
-            token.text match {
-              case (txt, "") =>
-                Failure(s + " expected,\nbut " + txt + " was found", in)
-              case (txt1, txt2) =>
-                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
-            }
+    def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
+      new Parser[(Elem, Token.Pos)] {
+        def apply(raw_input: Input) =
+        {
+          val in = proper(raw_input)
+          if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
+          else {
+            val pos =
+              in.pos match {
+                case pos: Token.Pos => pos
+                case _ => Token.Pos.none
+              }
+            val token = in.first
+            if (pred(token)) Success((token, pos), proper(in.rest))
+            else
+              token.text match {
+                case (txt, "") =>
+                  Failure(s + " expected,\nbut " + txt + " was found", in)
+                case (txt1, txt2) =>
+                  Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
+              }
+          }
         }
       }
-    }
 
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
-      token(s, pred) ^^ (_.content)
+      token(s, pred) ^^ { case (tok, _) => tok.content }
 
-    def command(name: String): Parser[String] =
-      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
+    def command(name: String): Parser[Position.T] =
+      token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
+        { case (_, pos) => pos.position }
 
     def keyword(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)

--- a/src/Pure/Isar/token.scala	Tue Apr 08 12:31:17 2014 +0200
+++ b/src/Pure/Isar/token.scala	Tue Apr 08 13:24:08 2014 +0200
@@ -121,25 +121,31 @@
 
   /* token reader */
 
-  class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position
+  object Pos
+  {
+    val none: Pos = new Pos(0, "")
+  }
+
+  final class Pos private[Token](val line: Int, val file: String)
+    extends scala.util.parsing.input.Position
   {
     def column = 0
     def lineContents = ""
-    override def toString =
-      if (file == "") ("line " + line.toString)
-      else ("line " + line.toString + " of " + quote(file))
 
-    def advance(token: Token): Position =
+    def advance(token: Token): Pos =
     {
       var n = 0
       for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Position(line + n, file)
+      if (n == 0) this else new Pos(line + n, file)
     }
+
+    def position: Position.T = Position.Line_File(line, file)
+    override def toString: String = Position.here(position)
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]
 
-  private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader
+  private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
   {
     def first = tokens.head
     def rest = new Token_Reader(tokens.tail, pos.advance(first))
@@ -147,7 +153,7 @@
   }
 
   def reader(tokens: List[Token], file: String = ""): Reader =
-    new Token_Reader(tokens, new Position(1, file))
+    new Token_Reader(tokens, new Pos(1, file))
 }
 
 

--- a/src/Pure/Tools/build.scala	Tue Apr 08 12:31:17 2014 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 08 13:24:08 2014 +0200
@@ -203,16 +203,14 @@
 
   private object Parser extends Parse.Parser
   {
-    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
-
-    def chapter(pos: Position.T): Parser[Chapter] =
+    val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
-    def session_entry(pos: Position.T): Parser[Session_Entry] =
+    val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
 
@@ -234,7 +232,7 @@
               ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep1(theories) ~
               ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
-        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
+        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
@@ -242,7 +240,7 @@
     {
       val toks = root_syntax.scan(File.read(root))
 
-      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
         case Success(result, _) =>
           var chapter = chapter_default
           val entries = new mutable.ListBuffer[(String, Session_Entry)]