# HG changeset patch
# User wenzelm
# Date 1520688027 -3600
# Node ID b123c9a007d0c67722984fe9d75db35eadc5250b
# Parent  33199d03350567cef6ef65898ddf088feab32e0d
tuned output;

diff -r 33199d033505 -r b123c9a007d0 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 10 14:11:58 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 10 14:20:27 2018 +0100
@@ -117,7 +117,7 @@
   sealed case class Info(name: String, port: Int, password: String)
   {
     override def toString: String =
-      "server " + quote(name) + " = " + print(port, password)
+      "server " + print_name_space(name) + "= " + print(port, password)
 
     def connection(): Connection =
     {
@@ -156,6 +156,9 @@
 
   /* per-user servers */
 
+  def print_name_space(name: String): String =
+    if (name == "") "" else quote(name) + " "
+
   def print(port: Int, password: String): String =
     "127.0.0.1:" + port + " (password " + quote(password) + ")"
 
@@ -200,8 +203,7 @@
             case Some(server_info) => (server_info, None)
             case None =>
               if (existing_server) {
-                if (name == "") error("Isabelle server not running")
-                else error("Isabelle server " + quote(name) + " not running")
+                  error("Isabelle server " + print_name_space(name) + "not running")
               }
 
               val server = new Server(port)