src/Pure/System/options.scala

   {
     def apply(name: String): String = get(name, Options.String, s => Some(s))
     def update(name: String, x: String): Options = put(name, Options.String, x)
   }
   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))
 
 
   /* external updates */

     def apply(name: String): String = value.string(name)
     def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
   }
   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)
 }