# HG changeset patch
# User wenzelm
# Date 1677059738 -3600
# Node ID a9decfa36e30b4b4ea9fa7db5bfd1b0a4125343d
# Parent  de7eae726f8ef846c47c0ac8b5af3c9f21b0787f
more operations;

diff -r de7eae726f8e -r a9decfa36e30 src/Pure/General/uuid.scala
--- 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)))
 }