src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Wed Sep 26 22:07:35 2018 +0200
+++ b/src/Pure/System/options.scala	Wed Sep 26 22:38:16 2018 +0200
@@ -280,6 +280,9 @@
   }
   val string = new String_Access
 
+  def proper_string(name: String): Option[String] =
+    Library.proper_string(string(name))
+
   def seconds(name: String): Time = Time.seconds(real(name))
 
 
@@ -443,5 +446,8 @@
   }
   val string = new String_Access
 
+  def proper_string(name: String): Option[String] =
+    Library.proper_string(string(name))
+
   def seconds(name: String): Time = value.seconds(name)
 }