equal
deleted
inserted
replaced
138 for (c <- token.content if c == '\n') n += 1 |
138 for (c <- token.content if c == '\n') n += 1 |
139 if (n == 0) this else new Pos(line + n, file) |
139 if (n == 0) this else new Pos(line + n, file) |
140 } |
140 } |
141 |
141 |
142 def position: Position.T = Position.Line_File(line, file) |
142 def position: Position.T = Position.Line_File(line, file) |
143 override def toString: String = Position.here(position) |
143 override def toString: String = Position.here_undelimited(position) |
144 } |
144 } |
145 |
145 |
146 abstract class Reader extends scala.util.parsing.input.Reader[Token] |
146 abstract class Reader extends scala.util.parsing.input.Reader[Token] |
147 |
147 |
148 private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader |
148 private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader |