src/Pure/General/uuid.scala
changeset 79717 da4e82434985
parent 77556 911548e4f228
--- a/src/Pure/General/uuid.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/General/uuid.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -11,6 +11,7 @@
   type T = java.util.UUID
 
   def random(): T = java.util.UUID.randomUUID()
+  def random_string(): String = random().toString
 
   def unapply(s: String): Option[T] =
     try { Some(java.util.UUID.fromString(s)) }