tuned signature;
authorwenzelm
Thu, 13 Dec 2018 17:01:20 +0100
changeset 69461 be142f577da6
parent 69460 5ffe7e17f770
child 69462 fe125722f7a9
tuned signature;
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)