src/Pure/ROOT.scala
changeset 69458 5655af3ea5bd
parent 69393 ed0824ef337e
child 71379 942cc80ba18a
equal deleted inserted replaced
69457:bea49e443909 69458:5655af3ea5bd
    19   val commas = Library.commas _
    19   val commas = Library.commas _
    20   val commas_quote = Library.commas_quote _
    20   val commas_quote = Library.commas_quote _
    21   def proper[A](x: A): Option[A] = Library.proper(x)
    21   def proper[A](x: A): Option[A] = Library.proper(x)
    22   val proper_string = Library.proper_string _
    22   val proper_string = Library.proper_string _
    23   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    23   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    24 
       
    25   type UUID = java.util.UUID
       
    26   def UUID(): UUID = java.util.UUID.randomUUID()
       
    27 }
    24 }