isabelle: src/Pure/General/uuid.scala@c15ee153dec1 (annotated)

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 }
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	20	}

author	wenzelm
	Wed, 20 Mar 2019 23:06:51 +0100
changeset 69933	c15ee153dec1
parent 69458	5655af3ea5bd
child 73133	497e11537d48
permissions	-rw-r--r--