author | wenzelm |
Mon, 30 May 2022 10:52:00 +0200 | |
changeset 75489 | f08fd5048df3 |
parent 75393 | 87ebf5a50283 |
child 77345 | a9decfa36e30 |
permissions | -rw-r--r-- |
/* Title: Pure/General/uuid.scala Author: Makarius Universally unique identifiers. */ package isabelle object UUID { type T = java.util.UUID def random(): T = java.util.UUID.randomUUID() 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)) }