isabelle: src/Pure/General/uuid.scala@2a0051496844 (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
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 74094 diff changeset	10	object UUID {
69458 5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	11	type T = java.util.UUID
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	12
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	13	def random(): T = java.util.UUID.randomUUID()
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	14
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	15	def unapply(s: String): Option[T] =
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	16	try { Some(java.util.UUID.fromString(s)) }
5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	17	catch { case _: IllegalArgumentException => None }
73133 497e11537d48 clarified signature: more operations; wenzelm parents: 69458 diff changeset	18
497e11537d48 clarified signature: more operations; wenzelm parents: 69458 diff changeset	19	def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
69458 5655af3ea5bd clarified modules and signature; wenzelm parents: diff changeset	20	}

author	wenzelm
	Fri, 05 Aug 2022 13:34:47 +0200
changeset 75761	2a0051496844
parent 75393	87ebf5a50283
child 77345	a9decfa36e30
permissions	-rw-r--r--