diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/Isar/token.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -157,10 +157,14 @@
 
   object Pos
   {
-    val none: Pos = new Pos(0, "")
+    val none: Pos = new Pos()
   }
 
-  final class Pos private[Token](val line: Int, val file: String)
+  final class Pos private[Token](
+      val line: Int = 0,
+      val offset: Symbol.Offset = 0,
+      val file: String = "",
+      val id: Document_ID.Generic = Document_ID.none)
     extends scala.util.parsing.input.Position
   {
     def column = 0
@@ -168,13 +172,27 @@
 
     def advance(token: Token): Pos =
     {
-      var n = 0
-      for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Pos(line + n, file)
+      var line1 = line
+      var offset1 = offset
+      for (s <- Symbol.iterator(token.source)) {
+        if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
+        if (offset1 > 0) offset1 += 1
+      }
+      if (line1 == line && offset1 == offset) this
+      else new Pos(line1, offset1, file, id)
     }
 
-    def position: Position.T = Position.Line_File(line, file)
-    override def toString: String = Position.here_undelimited(position)
+    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) :::
+      (if (file != "") Position.File(file) else Nil) :::
+      (if (id != Document_ID.none) Position.Id(id) else Nil)
+
+    def position(): Position.T = position(0)
+    def position(token: Token): Position.T = position(advance(token).offset)
+
+    override def toString: String = Position.here_undelimited(position())
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]
@@ -186,8 +204,8 @@
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token], file: String = ""): Reader =
-    new Token_Reader(tokens, new Pos(1, file))
+  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))
 }