src/Pure/General/uuid.scala
changeset 79717 da4e82434985
parent 77556 911548e4f228
equal deleted inserted replaced
79716:f33d37c171a9 79717:da4e82434985
     9 
     9 
    10 object UUID {
    10 object UUID {
    11   type T = java.util.UUID
    11   type T = java.util.UUID
    12 
    12 
    13   def random(): T = java.util.UUID.randomUUID()
    13   def random(): T = java.util.UUID.randomUUID()
       
    14   def random_string(): String = random().toString
    14 
    15 
    15   def unapply(s: String): Option[T] =
    16   def unapply(s: String): Option[T] =
    16     try { Some(java.util.UUID.fromString(s)) }
    17     try { Some(java.util.UUID.fromString(s)) }
    17     catch { case _: IllegalArgumentException => None }
    18     catch { case _: IllegalArgumentException => None }
    18 
    19