diff -r be5aa2c9c9ad -r 73a2f3fe0e8c src/Pure/General/json.scala --- 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) }