# HG changeset patch
# User wenzelm
# Date 1494185896 -7200
# Node ID ce909161d030fe21bfce74174629e96a0daad3ef
# Parent  a51290fd62d9b568d2c9c738b5a5b870d56925e1
more operations;

diff -r a51290fd62d9 -r ce909161d030 src/Pure/ROOT.scala
--- 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)
 }
diff -r a51290fd62d9 -r ce909161d030 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)
 }