changeset 77367 | d27d1224c67f |
parent 77007 | 19a7046f90f9 |
child 77372 | 44fe9fe96130 |
--- a/src/Pure/library.scala Fri Feb 24 12:40:40 2023 +0100 +++ b/src/Pure/library.scala Fri Feb 24 20:23:48 2023 +0100 @@ -283,6 +283,9 @@ def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) + def if_proper[A](x: Iterable[A], body: => String): String = + if (x == null || x.isEmpty) "" else body + /* reflection */