src/Pure/library.scala

--- 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)
 }