src/Pure/General/uuid.scala
author wenzelm
Sat, 08 Apr 2023 17:20:15 +0200
changeset 77787 b20ac2c26ea3
parent 77556 911548e4f228
child 79717 da4e82434985
permissions -rw-r--r--
clarified signature: more abstract;

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