tuned signature;

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

--- a/src/Pure/Thy/sessions.scala	Wed Sep 26 22:07:35 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Sep 26 22:38:16 2018 +0200
@@ -1108,7 +1108,7 @@
             host = options.string("build_database_host"),
             port = options.int("build_database_port"),
             ssh =
-              proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
+              options.proper_string("build_database_ssh_host").map(ssh_host =>
                 SSH.open_session(options,
                   host = ssh_host,
                   user = options.string("build_database_ssh_user"),