# HG changeset patch
# User wenzelm
# Date 1521211436 -3600
# Node ID 15027fb50a0cde2622468a2f688277c22b97f04e
# Parent  ff12c4556e2fd427de20ec1b40ba15c58037c8a6
clarified signature;

diff -r ff12c4556e2f -r 15027fb50a0c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 16 15:22:08 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 16 15:43:56 2018 +0100
@@ -66,7 +66,7 @@
       Map(
         "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
-        "shutdown" -> { case (context, ()) => context.shutdown(); () },
+        "shutdown" -> { case (context, ()) => context.server.close() },
         "cancel" -> { case (context, JSON.Value.String(id)) => context.cancel_task(id) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
@@ -78,8 +78,9 @@
               context.make_task(task =>
                 {
                   val (res, entry) =
-                    Server_Commands.Session_Start.command(task.progress, args, log = context.log)
-                  context.add_session(entry)
+                    Server_Commands.Session_Start.command(
+                      task.progress, args, log = context.server.log)
+                  context.server.add_session(entry)
                   res
                 })
           },
@@ -87,7 +88,7 @@
           { case (context, Server_Commands.Session_Stop(id)) =>
               context.make_task(_ =>
                 {
-                  val session = context.remove_session(id)
+                  val session = context.server.remove_session(id)
                   Server_Commands.Session_Stop.command(session)._1
                 })
           })
@@ -189,16 +190,10 @@
 
   /* context with output channels */
 
-  class Context private[Server](server: Server, connection: Connection)
+  class Context private[Server](val server: Server, connection: Connection)
   {
     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) }
     def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
@@ -211,8 +206,6 @@
     def progress(more: JSON.Object.Entry*): Connection_Progress =
       new Connection_Progress(context, more:_*)
 
-    def log: Logger = server.log
-
     override def toString: String = connection.toString
 
 
@@ -471,10 +464,10 @@
 {
   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 =
+  private val _sessions = Synchronized(Map.empty[String, Thy_Resources.Session])
+  def add_session(entry: (String, Thy_Resources.Session)) { _sessions.change(_ + entry) }
+  def get_session(id: String): Option[Thy_Resources.Session] = { _sessions.value.get(id) }
+  def remove_session(id: String): Thy_Resources.Session =
   {
     _sessions.change_result(sessions =>
       sessions.get(id) match {
diff -r ff12c4556e2f -r 15027fb50a0c src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 16 15:22:08 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 16 15:43: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, Thy_Resources.Session)) =
     {
       val base_info = Session_Build.command(progress, args.build)._3
 
@@ -131,7 +131,7 @@
     def unapply(json: JSON.T): Option[String] =
       JSON.string(json, "session_id")
 
-    def command(session: Session): (JSON.Object.T, Process_Result) =
+    def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
     {
       val result = session.stop()
       val result_json = JSON.Object("return_code" -> result.rc)