clarified server shutdown: stop all sessions;
authorwenzelm
Sun Mar 18 12:26:30 2018 +0100 (4 months ago)
changeset 67902c88044b10bbf
parent 67901 3e6864cf387f
child 67903 6e85d866251f
clarified server shutdown: stop all sessions;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Sun Mar 18 12:11:30 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Sun Mar 18 12:26:30 2018 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4        Map(
     1.5          "help" -> { case (_, ()) => table.keySet.toList.sorted },
     1.6          "echo" -> { case (_, t) => t },
     1.7 -        "shutdown" -> { case (context, ()) => context.server.close() },
     1.8 +        "shutdown" -> { case (context, ()) => context.server.shutdown() },
     1.9          "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
    1.10          "session_build" ->
    1.11            { case (context, Server_Commands.Session_Build(args)) =>
    1.12 @@ -484,6 +484,8 @@
    1.13  {
    1.14    server =>
    1.15  
    1.16 +  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
    1.17 +
    1.18    private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
    1.19    def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
    1.20    def the_session(id: UUID): Thy_Resources.Session =
    1.21 @@ -498,9 +500,19 @@
    1.22        })
    1.23    }
    1.24  
    1.25 -  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
    1.26 +  def shutdown()
    1.27 +  {
    1.28 +    server_socket.close
    1.29  
    1.30 -  def close() { server_socket.close }
    1.31 +    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
    1.32 +    for ((_, session) <- sessions) {
    1.33 +      try {
    1.34 +        val result = session.stop()
    1.35 +        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
    1.36 +      }
    1.37 +      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
    1.38 +    }
    1.39 +  }
    1.40  
    1.41    def port: Int = server_socket.getLocalPort
    1.42    val password: String = UUID().toString
    1.43 @@ -574,5 +586,5 @@
    1.44  
    1.45    def start { server_thread }
    1.46  
    1.47 -  def join { server_thread.join; close() }
    1.48 +  def join { server_thread.join; shutdown() }
    1.49  }