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