--- a/src/Pure/General/antiquote.scala Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/General/antiquote.scala Fri Apr 08 16:26:48 2022 +0200
@@ -44,7 +44,8 @@
/* read */
def read(input: CharSequence): List[Antiquote] = {
- Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match {
+ val result = Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input))
+ (result : @unchecked) match {
case Parsers.Success(xs, _) => xs
case Parsers.NoSuccess(_, next) =>
error("Malformed quotation/antiquotation source" +
--- a/src/Pure/General/json.scala Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/General/json.scala Fri Apr 08 16:26:48 2022 +0200
@@ -145,7 +145,8 @@
def parse(input: CharSequence, strict: Boolean): T = {
val scanner = new Lexer.Scanner(Scan.char_reader(input))
- phrase(if (strict) json_object | json_array else json_value)(scanner) match {
+ val result = phrase(if (strict) json_object | json_array else json_value)(scanner)
+ (result : @unchecked) match {
case Success(json, _) => json
case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos)
}
--- 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)
--- a/src/Pure/ML/ml_lex.scala Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala Fri Apr 08 16:26:48 2022 +0200
@@ -281,7 +281,8 @@
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
+ val result = Parsers.parse(Parsers.token_line(SML, 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)
--- a/src/Pure/Thy/bibtex.scala Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala Fri Apr 08 16:26:48 2022 +0200
@@ -599,7 +599,8 @@
val chunks = new mutable.ListBuffer[Chunk]
var ctxt = context
while (!in.atEnd) {
- Parsers.parse(Parsers.chunk_line(ctxt), in) match {
+ val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
+ (result : @unchecked) match {
case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
case Parsers.NoSuccess(_, rest) =>
error("Unepected failure to parse input:\n" + rest.source.toString)