changeset 65761 | ce909161d030 |
parent 65715 | e57e5935c6b4 |
child 67885 | 839a624aabb9 |
--- a/src/Pure/ROOT.scala Sun May 07 17:40:41 2017 +0200 +++ b/src/Pure/ROOT.scala Sun May 07 21:38:16 2017 +0200 @@ -18,5 +18,7 @@ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ + def proper[A](x: A): Option[A] = Library.proper(x) val proper_string = Library.proper_string _ + def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) }