src/Pure/General/uuid.scala
author wenzelm
Fri, 18 Jun 2021 12:12:28 +0200
changeset 73862 38fe15a42ff2
parent 73133 497e11537d48
child 74094 6113f1db4342
permissions -rw-r--r--
tuned signature;
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
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
     4
Universally unique identifiers.
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
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    10
object UUID
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    11
{
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    12
  type T = java.util.UUID
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    13
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    14
  def random(): T = java.util.UUID.randomUUID()
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    15
  def random_string(): String = random().toString
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    16
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    17
  def unapply(s: String): Option[T] =
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    18
    try { Some(java.util.UUID.fromString(s)) }
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    19
    catch { case _: IllegalArgumentException => None }
73133
497e11537d48 clarified signature: more operations;
wenzelm
parents: 69458
diff changeset
    20
497e11537d48 clarified signature: more operations;
wenzelm
parents: 69458
diff changeset
    21
  def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents:
diff changeset
    22
}