src/Pure/ROOT.scala
changeset 76176 d6bd84eb94a3
parent 75393 87ebf5a50283
child 76537 cdbe20024038
equal deleted inserted replaced
76175:4ff3cea76201 76176:d6bd84eb94a3
    19   val commas_quote = Library.commas_quote _
    19   val commas_quote = Library.commas_quote _
    20   val proper_bool = Library.proper_bool _
    20   val proper_bool = Library.proper_bool _
    21   val proper_string = Library.proper_string _
    21   val proper_string = Library.proper_string _
    22   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    22   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    23 }
    23 }
       
    24