# HG changeset patch
# User wenzelm
# Date 1544716880 -3600
# Node ID be142f577da6356c47d6e17a2605efd42b9b5dbc
# Parent  5ffe7e17f770a959a5f9bdb116b3331c20fb4e76
tuned signature;

diff -r 5ffe7e17f770 -r be142f577da6 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Dec 13 16:36:26 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Dec 13 17:01:20 2018 +0100
@@ -307,10 +307,10 @@
 
   /* server info */
 
-  def print_socket(port: Int): String = "127.0.0.1:" + port
+  def print_address(port: Int): String = "127.0.0.1:" + port
 
   def print(port: Int, password: String): String =
-    print_socket(port) + " (password " + quote(password) + ")"
+    print_address(port) + " (password " + quote(password) + ")"
 
   object Info
   {
@@ -328,7 +328,7 @@
 
   class Info private(val name: String, val port: Int, val password: String)
   {
-    def socket_name: String = print_socket(port)
+    def address: String = print_address(port)
 
     override def toString: String =
       "server " + quote(name) + " = " + print(port, password)