src/Pure/General/uuid.scala
author wenzelm
Sat, 24 Jul 2021 15:38:41 +0200
changeset 74056 fb8d5c0133c9
parent 73133 497e11537d48
child 74094 6113f1db4342
permissions -rw-r--r--
clarified 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
}