# HG changeset patch
# User wenzelm
# Date 1677266628 -3600
# Node ID d27d1224c67f03c271de97e8eef4d1bb413065b4
# Parent  8d6ba14f9d22fa87a9c25e4ab4ad9b51d2eb56eb
more operations;

diff -r 8d6ba14f9d22 -r d27d1224c67f src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Fri Feb 24 12:40:40 2023 +0100
+++ b/src/Pure/ROOT.scala	Fri Feb 24 20:23:48 2023 +0100
@@ -20,5 +20,6 @@
   val proper_bool = Library.proper_bool _
   val proper_string = Library.proper_string _
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
+  def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
 }
 
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 */