Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more operations;
authorwenzelm
Fri, 24 Feb 2023 20:23:48 +0100
changeset 77367 d27d1224c67f
parent 77366 8d6ba14f9d22
child 77368 7c57d9586f4c
more operations;
src/Pure/ROOT.scala file | annotate | diff | comparison | revisions
src/Pure/library.scala file | annotate | diff | comparison | revisions 
--- 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)
 }
 
--- 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 */
isabelle