changeset 73340 | 0ffcad1f6130 |
parent 73317 | df49ca5da9d0 |
child 73359 | d8a0e996614b |
--- a/src/Pure/Thy/bibtex.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/Thy/bibtex.scala Mon Mar 01 22:22:12 2021 +0100 @@ -87,7 +87,7 @@ def make_pos(length: Int): Position.T = Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line) - def advance_pos(tok: Token) + def advance_pos(tok: Token): Unit = { for (s <- Symbol.iterator(tok.source)) { if (Symbol.is_newline(s)) line += 1