69458
|
1 |
/* Title: Pure/General/uuid.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
77556
|
4 |
Universally Unique Identifiers.
|
69458
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
75393
|
10 |
object UUID {
|
69458
|
11 |
type T = java.util.UUID
|
|
12 |
|
|
13 |
def random(): T = java.util.UUID.randomUUID()
|
79717
|
14 |
def random_string(): String = random().toString
|
69458
|
15 |
|
|
16 |
def unapply(s: String): Option[T] =
|
|
17 |
try { Some(java.util.UUID.fromString(s)) }
|
|
18 |
catch { case _: IllegalArgumentException => None }
|
73133
|
19 |
|
|
20 |
def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
|
77345
|
21 |
|
|
22 |
def make(s: String): T =
|
|
23 |
unapply(s).getOrElse(error("Bad UUID: " + quote(s)))
|
69458
|
24 |
}
|