changeset 73344 | f5c147654661 |
parent 73340 | 0ffcad1f6130 |
child 73359 | d8a0e996614b |
--- a/src/Pure/Thy/thy_syntax.scala Mon Mar 01 22:50:00 2021 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 01 23:17:47 2021 +0100 @@ -275,7 +275,7 @@ var last = last_visible var i = 0 while (i < reparse_limit && it.hasNext) { - last = it.next + last = it.next() i += last.length } reparse_spans(resources, syntax, get_blob, can_import,