--- a/src/Pure/ROOT.scala Sat Mar 11 13:37:58 2023 +0100
+++ b/src/Pure/ROOT.scala Sat Mar 11 14:18:56 2023 +0100
@@ -25,4 +25,5 @@
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)
+ def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
}
--- a/src/Pure/System/options.scala Sat Mar 11 13:37:58 2023 +0100
+++ b/src/Pure/System/options.scala Sat Mar 11 14:18:56 2023 +0100
@@ -250,7 +250,7 @@
override def toString: String = iterator.mkString("Options(", ",", ")")
private def print_entry(opt: Options.Entry): String =
- if (opt.public) "public " + opt.print else opt.print
+ if_proper(opt.public, "public ") + opt.print
def print: String = cat_lines(iterator.toList.sortBy(_.name).map(print_entry))
--- a/src/Pure/library.scala Sat Mar 11 13:37:58 2023 +0100
+++ b/src/Pure/library.scala Sat Mar 11 14:18:56 2023 +0100
@@ -292,6 +292,9 @@
def if_proper[A](x: Iterable[A], body: => String): String =
if (x == null || x.isEmpty) "" else body
+ def if_proper(b: Boolean, body: => String): String =
+ if (!b) "" else body
+
/* reflection */