src/Pure/General/uuid.scala
changeset 73133 497e11537d48
parent 69458 5655af3ea5bd
child 74094 6113f1db4342
--- a/src/Pure/General/uuid.scala	Fri Jan 15 14:11:01 2021 +0100
+++ b/src/Pure/General/uuid.scala	Sat Jan 16 15:43:54 2021 +0100
@@ -17,4 +17,6 @@
   def unapply(s: String): Option[T] =
     try { Some(java.util.UUID.fromString(s)) }
     catch { case _: IllegalArgumentException => None }
+
+  def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
 }