# HG changeset patch
# User wenzelm
# Date 1520777730 -3600
# Node ID 82fb12061069973a12bd1aa1dd8fde4e311585f4
# Parent  e30d6368c7c8555f7e397ddeb904dae1d43b88ab
more uniform output: this may be parsed by another program;

diff -r e30d6368c7c8 -r 82fb12061069 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Mar 11 15:08:14 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sun Mar 11 15:15:30 2018 +0100
@@ -154,7 +154,7 @@
   sealed case class Info(name: String, port: Int, password: String)
   {
     override def toString: String =
-      "server " + print_name_space(name) + "= " + print(port, password)
+      "server " + quote(name) + " = " + print(port, password)
 
     def connection(): Connection =
     {
@@ -193,9 +193,6 @@
 
   /* 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) + ")"
 
@@ -239,9 +236,7 @@
           find(db, name) match {
             case Some(server_info) => (server_info, None)
             case None =>
-              if (existing_server) {
-                  error("Isabelle server " + print_name_space(name) + "not running")
-              }
+              if (existing_server) error("Isabelle server " + quote(name) + " not running")
 
               val server = new Server(port)
               val server_info = Info(name, server.port, server.password)