more operations;

--- 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)))
   }