# 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() } }