# HG changeset patch
# User wenzelm
# Date 1493902699 -7200
# Node ID 556c34fd0554aa81ae5accead93f5079fc66fa0b
# Parent  678e00851cfb35a2c1ec45d0f5302102826dfb24
tuned;

diff -r 678e00851cfb -r 556c34fd0554 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu May 04 14:57:31 2017 +0200
+++ b/src/Pure/General/sql.scala	Thu May 04 14:58:19 2017 +0200
@@ -387,9 +387,9 @@
 
     if (user == "") error("Undefined database user")
 
-    val db_host = if (host != "") host else "localhost"
+    val db_host = proper_string(host) getOrElse "localhost"
     val db_port = if (port > 0 && port != default_port) ":" + port else ""
-    val db_name = "/" + (if (database != "") database else user)
+    val db_name = "/" + (proper_string(database) getOrElse user)
 
     val (url, name, port_forwarding) =
       ssh match {
diff -r 678e00851cfb -r 556c34fd0554 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu May 04 14:57:31 2017 +0200
+++ b/src/Pure/General/ssh.scala	Thu May 04 14:58:19 2017 +0200
@@ -77,7 +77,8 @@
     def open_session(host: String, user: String = "", port: Int = 0): Session =
     {
       val session =
-        jsch.getSession(if (user == "") null else user, host, if (port > 0) port else default_port)
+        jsch.getSession(proper_string(user) getOrElse null, host,
+          if (port > 0) port else default_port)
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))
diff -r 678e00851cfb -r 556c34fd0554 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Thu May 04 14:57:31 2017 +0200
+++ b/src/Pure/PIDE/command_span.scala	Thu May 04 14:58:19 2017 +0200
@@ -15,7 +15,7 @@
   sealed abstract class Kind {
     override def toString: String =
       this match {
-        case Command_Span(name, _) => if (name != "") name else "<command>"
+        case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
         case Ignored_Span => "<ignored>"
         case Malformed_Span => "<malformed>"
       }
diff -r 678e00851cfb -r 556c34fd0554 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu May 04 14:57:31 2017 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu May 04 14:58:19 2017 +0200
@@ -139,11 +139,8 @@
     env.getOrElse(name, "")
 
   def getenv_strict(name: String, env: Map[String, String] = settings()): String =
-  {
-    val value = getenv(name, env)
-    if (value != "") value
-    else error("Undefined Isabelle environment variable: " + quote(name))
-  }
+    proper_string(getenv(name, env)) getOrElse
+      error("Undefined Isabelle environment variable: " + quote(name))
 
   def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")