isabelle: src/Pure/General/uuid.scala@6113f1db4342 (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
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	16	def unapply(s: String): Option[T] =
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	17	try { Some(java.util.UUID.fromString(s)) }
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	18	catch { case _: IllegalArgumentException => None }
73133 497e11537d48 clarified signature: more operations; wenzelm parents: 69458 diff changeset	19
497e11537d48 clarified signature: more operations; wenzelm parents: 69458 diff changeset	20	def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
69458 5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	21	}

author	wenzelm
	Sat, 31 Jul 2021 15:44:11 +0200
changeset 74094	6113f1db4342
parent 73133	497e11537d48
child 75393	87ebf5a50283
permissions	-rw-r--r--