# HG changeset patch
# User wenzelm
# Date 1521372390 -3600
# Node ID c88044b10bbfc0cd8a4465505bf19b253ae4d824
# Parent  3e6864cf387ff69558decd660e1f5ffbec1e12e6
clarified server shutdown: stop all sessions;

diff -r 3e6864cf387f -r c88044b10bbf src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Mar 18 12:11:30 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sun Mar 18 12:26:30 2018 +0100
@@ -66,7 +66,7 @@
       Map(
         "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
-        "shutdown" -> { case (context, ()) => context.server.close() },
+        "shutdown" -> { case (context, ()) => context.server.shutdown() },
         "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
@@ -484,6 +484,8 @@
 {
   server =>
 
+  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+
   private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
   def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
   def the_session(id: UUID): Thy_Resources.Session =
@@ -498,9 +500,19 @@
       })
   }
 
-  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+  def shutdown()
+  {
+    server_socket.close
 
-  def close() { server_socket.close }
+    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
+    for ((_, session) <- sessions) {
+      try {
+        val result = session.stop()
+        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
+      }
+      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
+    }
+  }
 
   def port: Int = server_socket.getLocalPort
   val password: String = UUID().toString
@@ -574,5 +586,5 @@
 
   def start { server_thread }
 
-  def join { server_thread.join; close() }
+  def join { server_thread.join; shutdown() }
 }