--- a/src/Pure/ROOT.scala Thu May 04 11:34:42 2017 +0200
+++ b/src/Pure/ROOT.scala Thu May 04 12:15:50 2017 +0200
@@ -18,4 +18,6 @@
val quote = Library.quote _
val commas = Library.commas _
val commas_quote = Library.commas_quote _
+ val proper_string = Library.proper_string _
+ val proper_string_default = Library.proper_string_default _
}
--- a/src/Pure/library.scala Thu May 04 11:34:42 2017 +0200
+++ b/src/Pure/library.scala Thu May 04 12:15:50 2017 +0200
@@ -144,6 +144,12 @@
def trim_substring(s: String): String = new String(s.toCharArray)
+ def proper_string(s: String): Option[String] =
+ if (s == "") None else Some(s)
+
+ def proper_string_default(s: String, default: => String): String =
+ if (s == "") default else s
+
/* quote */