more operations;

--- a/src/Pure/General/uuid.scala	Tue Feb 21 14:36:04 2023 +0100
+++ b/src/Pure/General/uuid.scala	Wed Feb 22 10:55:38 2023 +0100
@@ -17,4 +17,7 @@
     catch { case _: IllegalArgumentException => None }
 
   def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
+
+  def make(s: String): T =
+    unapply(s).getOrElse(error("Bad UUID: " + quote(s)))
 }