diff -r b5eb7c688836 -r 740a0ca7e09b src/Pure/Isar/token.scala --- 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) }