more operations;

--- a/src/Pure/ROOT.scala	Sun May 07 17:40:41 2017 +0200
+++ b/src/Pure/ROOT.scala	Sun May 07 21:38:16 2017 +0200
@@ -18,5 +18,7 @@
   val quote = Library.quote _
   val commas = Library.commas _
   val commas_quote = Library.commas_quote _
+  def proper[A](x: A): Option[A] = Library.proper(x)
   val proper_string = Library.proper_string _
+  def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
 }

--- a/src/Pure/library.scala	Sun May 07 17:40:41 2017 +0200
+++ b/src/Pure/library.scala	Sun May 07 21:38:16 2017 +0200
@@ -144,9 +144,6 @@
 
   def trim_substring(s: String): String = new String(s.toCharArray)
 
-  def proper_string(s: String): Option[String] =
-    if (s == null || s == "") None else Some(s)
-
 
   /* quote */
 
@@ -247,4 +244,16 @@
     dups(lst)
     result.toList
   }
+
+
+  /* proper values */
+
+  def proper[A](x: A): Option[A] =
+    if (x == null) None else Some(x)
+
+  def proper_string(s: String): Option[String] =
+    if (s == null || s == "") None else Some(s)
+
+  def proper_list[A](list: List[A]): Option[List[A]] =
+    if (list == null || list.isEmpty) None else Some(list)
 }