src/Pure/library.scala

     if (s == null || s == "") None else Some(s)
 
   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 */
 
   def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = {
     import scala.language.existentials