src/Pure/Thy/bibtex.scala
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