| author | wenzelm |
| Thu, 22 Feb 2024 20:37:53 +0100 | |
| changeset 79707 | 4ded6d260db0 |
| parent 77556 | 911548e4f228 |
| child 79717 | da4e82434985 |
| 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)) def make(s: String): T = unapply(s).getOrElse(error("Bad UUID: " + quote(s))) }