tuned signature;
authorwenzelm
Fri, 09 Mar 2018 13:07:00 +0100
changeset 67791 acecef5fad58
parent 67790 1babcc248be0
child 67792 73c7a55972b4
tuned signature;
src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 13:03:55 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 13:07:00 2018 +0100
@@ -20,7 +20,7 @@
     Map(
       "echo" -> { case (_, t) => t },
       "help" -> { case (_, JSON.empty) => commands.keySet.toList.sorted },
-      "shutdown" -> { case (server, JSON.empty) => server.shutdown(); JSON.empty })
+      "shutdown" -> { case (server, JSON.empty) => server.close(); JSON.empty })
 
   object Reply extends Enumeration
   {
@@ -203,6 +203,9 @@
   server =>
 
   private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+
+  def close() { server_socket.close }
+
   def port: Int = server_socket.getLocalPort
   val password: String = Library.UUID()
 
@@ -261,7 +264,5 @@
 
   def start { server_thread }
 
-  def join { server_thread.join; shutdown() }
-
-  def shutdown() { server_socket.close }
+  def join { server_thread.join; close() }
 }