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