# HG changeset patch
# User wenzelm
# Date 1544715386 -3600
# Node ID 5ffe7e17f770a959a5f9bdb116b3331c20fb4e76
# Parent  bbb61a9cb99adaca2381230f8b563fd47d0dfe29
clarified signature, e.g. for re-use by other servers;

diff -r bbb61a9cb99a -r 5ffe7e17f770 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Dec 13 15:32:54 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Dec 13 16:36:26 2018 +0100
@@ -307,8 +307,29 @@
 
   /* server info */
 
-  sealed case class Info(name: String, port: Int, password: String)
+  def print_socket(port: Int): String = "127.0.0.1:" + port
+
+  def print(port: Int, password: String): String =
+    print_socket(port) + " (password " + quote(password) + ")"
+
+  object Info
   {
+    private val Pattern = """server "([^"]*)" = 127\.0\.0\.1:(\d+) \(password "([^"]*)"\)""".r
+
+    def unapply(s: String): Option[Info] =
+      s match {
+        case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password))
+        case _ => None
+      }
+
+    def apply(name: String, port: Int, password: String): Info =
+      new Info(name, port, password)
+  }
+
+  class Info private(val name: String, val port: Int, val password: String)
+  {
+    def socket_name: String = print_socket(port)
+
     override def toString: String =
       "server " + quote(name) + " = " + print(port, password)
 
@@ -342,9 +363,6 @@
 
   val default_name = "isabelle"
 
-  def print(port: Int, password: String): String =
-    "127.0.0.1:" + port + " (password " + quote(password) + ")"
-
   object Data
   {
     val database = Path.explode("$ISABELLE_HOME_USER/servers.db")