src/Pure/General/json.scala
changeset 75420 73a2f3fe0e8c
parent 75406 85e8b4c2b9a9
child 75957 515b17021c91
--- 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)
       }