| author | wenzelm |
| Wed, 26 May 2021 18:07:49 +0200 | |
| changeset 73787 | 493b1ae188da |
| parent 73133 | 497e11537d48 |
| child 74094 | 6113f1db4342 |
| 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 random_string(): String = random().toString 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)) }