diff -r 8d6ba14f9d22 -r d27d1224c67f src/Pure/library.scala
--- 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 */