# HG changeset patch
# User wenzelm
# Date 1493892950 -7200
# Node ID ddd6dfc28e80014a574e47e7592cbcb337ac2570
# Parent  ff8a7f20ff327f6d49dea60b257877632c0531ae
more operations;

diff -r ff8a7f20ff32 -r ddd6dfc28e80 src/Pure/ROOT.scala
--- 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 _
 }
diff -r ff8a7f20ff32 -r ddd6dfc28e80 src/Pure/library.scala
--- 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 */