src/Pure/Isar/token.scala

     extends input.Position
   {
     def column = 0
     def lineContents = ""
 
-    def advance(token: Token): Pos =
+    def advance(token: Token): Pos = advance(token.source)
+    def advance(source: String): Pos =
     {
       var line1 = line
       var offset1 = offset
-      for (s <- Symbol.iterator(token.source)) {
+      for (s <- Symbol.iterator(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)

       (if (file != "") Position.File(file) else Nil) :::
       (if (id != "") Position.Id_String(id) else Nil)
 
     def position(): Position.T = position(0)
     def position(token: Token): Position.T = position(advance(token).offset)
+    def position(source: String): Position.T = position(advance(source).offset)
 
     override def toString: String = Position.here(position(), delimited = false)
   }
 
   abstract class Reader extends input.Reader[Token]