src/Pure/General/uuid.scala
author wenzelm
Sat, 01 Jun 2024 12:35:38 +0200
changeset 80225 d9ff4296e3b7
parent 79717 da4e82434985
permissions -rw-r--r--
unused;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/uuid.scala
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     3
77556
911548e4f228 tuned comments;
wenzelm
parents: 77345
diff changeset
     4
Universally Unique Identifiers.
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     5
*/
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     6
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     7
package isabelle
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     8
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74094
diff changeset
    10
object UUID {
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    11
  type T = java.util.UUID
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    12
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    13
  def random(): T = java.util.UUID.randomUUID()
79717
da4e82434985 tuned signature;
wenzelm
parents: 77556
diff changeset
    14
  def random_string(): String = random().toString
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    15
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    16
  def unapply(s: String): Option[T] =
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    17
    try { Some(java.util.UUID.fromString(s)) }
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    18
    catch { case _: IllegalArgumentException => None }
73133
497e11537d48 clarified signature: more operations;
wenzelm
parents: 69458
diff changeset
    19
497e11537d48 clarified signature: more operations;
wenzelm
parents: 69458
diff changeset
    20
  def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
77345
a9decfa36e30 more operations;
wenzelm
parents: 75393
diff changeset
    21
a9decfa36e30 more operations;
wenzelm
parents: 75393
diff changeset
    22
  def make(s: String): T =
a9decfa36e30 more operations;
wenzelm
parents: 75393
diff changeset
    23
    unapply(s).getOrElse(error("Bad UUID: " + quote(s)))
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    24
}