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