# HG changeset patch
# User wenzelm
# Date 1521148676 -3600
# Node ID 195ff117894c6f6b93bae5ddec9b5625378c90f8
# Parent  586be47e00b30b019cfb693c36382fea65e43796
store session: per Server/Context, not Connection;
support for "session_stop";

diff -r 586be47e00b3 -r 195ff117894c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 15 21:44:34 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 15 22:17:56 2018 +0100
@@ -77,11 +77,19 @@
           { case (context, Server_Commands.Session_Start(args)) =>
               context.make_task(task =>
                 {
-                  val (res, session_id, session) =
+                  val (res, entry) =
                     Server_Commands.Session_Start.command(task.progress, args, log = context.log)
-                  // FIXME store session in context
+                  context.add_session(entry)
                   res
                 })
+          },
+        "session_stop" ->
+          { case (context, Server_Commands.Session_Stop(id)) =>
+              context.make_task(_ =>
+                {
+                  val session = context.remove_session(id)
+                  Server_Commands.Session_Stop.command(session)._1
+                })
           })
 
     def unapply(name: String): Option[T] = table.get(name)
@@ -185,6 +193,10 @@
   {
     context =>
 
+    def add_session(entry: (String, Session)) { server.add_session(entry) }
+    def get_session(id: String): Option[Session] = { server.get_session(id) }
+    def remove_session(id: String): Session = { server.remove_session(id) }
+
     def shutdown() { server.close() }
 
     def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
@@ -459,6 +471,18 @@
 {
   server =>
 
+  private val _sessions = Synchronized(Map.empty[String, Session])
+  def add_session(entry: (String, Session)) { _sessions.change(_ + entry) }
+  def get_session(id: String): Option[Session] = { _sessions.value.get(id) }
+  def remove_session(id: String): Session =
+  {
+    _sessions.change_result(sessions =>
+      sessions.get(id) match {
+        case Some(session) => (session, sessions - id)
+        case None => error("No session " + quote(id))
+      })
+  }
+
   private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
 
   def close() { server_socket.close }
diff -r 586be47e00b3 -r 195ff117894c src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Thu Mar 15 21:44:34 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 15 22:17:56 2018 +0100
@@ -105,7 +105,7 @@
       yield Args(build = build, print_mode = print_mode)
 
     def command(progress: Progress, args: Args, log: Logger = No_Logger)
-      : (JSON.Object.T, String, Session) =
+      : (JSON.Object.T, (String, Session)) =
     {
       val base_info = Session_Build.command(progress, args.build)._3
 
@@ -122,7 +122,22 @@
       val id = Library.UUID()
       val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id)
 
-      (res, id, session)
+      (res, id -> session)
+    }
+  }
+
+  object Session_Stop
+  {
+    def unapply(json: JSON.T): Option[String] =
+      JSON.string(json, "session_id")
+
+    def command(session: Session): (JSON.Object.T, Process_Result) =
+    {
+      val result = session.stop()
+      val result_json = JSON.Object("return_code" -> result.rc)
+
+      if (result.ok) (result_json, result)
+      else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
     }
   }
 }