# HG changeset patch
# User wenzelm
# Date 1677098128 -3600
# Node ID 739a9c34c538b8252d200597b70e5c41b51a3d0f
# Parent  cf2ef4be36306349102abc9d33882730fb065154
more operations;

diff -r cf2ef4be3630 -r 739a9c34c538 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Wed Feb 22 21:31:36 2023 +0100
+++ b/src/Pure/General/json.scala	Wed Feb 22 21:35:28 2023 +0100
@@ -33,6 +33,9 @@
           Some(m.asInstanceOf[Object.T])
         case _ => None
       }
+
+    def parse(s: S): Object.T =
+      unapply(JSON.parse(s)).getOrElse(error("Bad JSON object " + quote(s)))
   }