--- a/src/Pure/Isar/token.scala Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/Isar/token.scala Fri Apr 08 16:26:48 2022 +0200
@@ -140,7 +140,8 @@
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {
+ val result = Parsers.parse(Parsers.token_line(keywords, ctxt), in)
+ (result : @unchecked) match {
case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
case Parsers.NoSuccess(_, rest) =>
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)