# HG changeset patch
# User wenzelm
# Date 1520597220 -3600
# Node ID acecef5fad588fbc8bab3a7feadfe643dfdb3db0
# Parent  1babcc248be0f7e31569d4bc44bdfa74a87eb029
tuned signature;

diff -r 1babcc248be0 -r acecef5fad58 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() }
 }