# HG changeset patch
# User wenzelm
# Date 1610653629 -3600
# Node ID ff6b5e468d5f790a3484fea4a9ebee7a253b7e00
# Parent  5f8f7746b4aa7906443ce7cde5d3b09074c584a3
clarified signature: support more generic server implementations;

diff -r 5f8f7746b4aa -r ff6b5e468d5f src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Wed Jan 13 12:22:59 2021 +0100
+++ b/src/Pure/Tools/server.scala	Thu Jan 14 20:47:09 2021 +0100
@@ -121,6 +121,38 @@
   }
 
 
+  /* handler: port, password, thread */
+
+  abstract class Handler(port0: Int)
+  {
+    val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
+    def port: Int = socket.getLocalPort
+    val password: String = UUID.random_string()
+
+    override def toString: String = print(port, password)
+
+    def handle(connection: Server.Connection): Unit
+
+    private lazy val thread: Thread =
+      Isabelle_Thread.fork(name = "server_handler") {
+        var finished = false
+        while (!finished) {
+          Exn.capture(socket.accept) match {
+            case Exn.Res(client) =>
+              Isabelle_Thread.fork(name = "server_connection") {
+                using(Connection(client))(connection =>
+                  if (connection.read_password(password)) handle(connection))
+              }
+            case Exn.Exn(_) => finished = true
+          }
+        }
+      }
+
+    def start { thread }
+    def join { thread.join }
+  }
+
+
   /* socket connection */
 
   object Connection
@@ -477,12 +509,10 @@
     })
 }
 
-class Server private(_port: Int, val log: Logger)
+class Server private(port0: Int, val log: Logger) extends Server.Handler(port0)
 {
   server =>
 
-  private val server_socket = new ServerSocket(_port, 50, Server.localhost)
-
   private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
   def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
   def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
@@ -498,7 +528,7 @@
 
   def shutdown()
   {
-    server_socket.close
+    server.socket.close
 
     val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
     for ((_, session) <- sessions) {
@@ -510,75 +540,53 @@
     }
   }
 
-  def port: Int = server_socket.getLocalPort
-  val password: String = UUID.random_string()
+  override def join { super.join; shutdown() }
 
-  override def toString: String = Server.print(port, password)
-
-  private def handle(connection: Server.Connection)
+  override def handle(connection: Server.Connection)
   {
     using(new Server.Context(server, connection))(context =>
     {
-      if (connection.read_password(password)) {
-        connection.reply_ok(
-          JSON.Object(
-            "isabelle_id" -> Isabelle_System.isabelle_id(),
-            "isabelle_version" -> Distribution.version))
+      connection.reply_ok(
+        JSON.Object(
+          "isabelle_id" -> Isabelle_System.isabelle_id(),
+          "isabelle_version" -> Distribution.version))
 
-        var finished = false
-        while (!finished) {
-          connection.read_message() match {
-            case None => finished = true
-            case Some("") => context.notify("Command 'help' provides list of commands")
-            case Some(msg) =>
-              val (name, argument) = Server.Argument.split(msg)
-              Server.command_table.get(name) match {
-                case Some(cmd) =>
-                  argument match {
-                    case Server.Argument(arg) =>
-                      if (cmd.command_body.isDefinedAt((context, arg))) {
-                        Exn.capture { cmd.command_body((context, arg)) } match {
-                          case Exn.Res(task: Server.Task) =>
-                            connection.reply_ok(JSON.Object(task.ident))
-                            task.start
-                          case Exn.Res(res) => connection.reply_ok(res)
-                          case Exn.Exn(exn) =>
-                            val err = Server.json_error(exn)
-                            if (err.isEmpty) throw exn else connection.reply_error(err)
-                        }
+      var finished = false
+      while (!finished) {
+        connection.read_message() match {
+          case None => finished = true
+          case Some("") => context.notify("Command 'help' provides list of commands")
+          case Some(msg) =>
+            val (name, argument) = Server.Argument.split(msg)
+            Server.command_table.get(name) match {
+              case Some(cmd) =>
+                argument match {
+                  case Server.Argument(arg) =>
+                    if (cmd.command_body.isDefinedAt((context, arg))) {
+                      Exn.capture { cmd.command_body((context, arg)) } match {
+                        case Exn.Res(task: Server.Task) =>
+                          connection.reply_ok(JSON.Object(task.ident))
+                          task.start
+                        case Exn.Res(res) => connection.reply_ok(res)
+                        case Exn.Exn(exn) =>
+                          val err = Server.json_error(exn)
+                          if (err.isEmpty) throw exn else connection.reply_error(err)
                       }
-                      else {
-                        connection.reply_error_message(
-                          "Bad argument for command " + Library.single_quote(name),
-                          "argument" -> argument)
-                      }
-                    case _ =>
+                    }
+                    else {
                       connection.reply_error_message(
-                        "Malformed argument for command " + Library.single_quote(name),
+                        "Bad argument for command " + Library.single_quote(name),
                         "argument" -> argument)
-                  }
-                case None => connection.reply_error("Bad command " + Library.single_quote(name))
-              }
-          }
+                    }
+                  case _ =>
+                    connection.reply_error_message(
+                      "Malformed argument for command " + Library.single_quote(name),
+                      "argument" -> argument)
+                }
+              case None => connection.reply_error("Bad command " + Library.single_quote(name))
+            }
         }
       }
     })
   }
-
-  private lazy val server_thread: Thread =
-    Isabelle_Thread.fork(name = "server") {
-      var finished = false
-      while (!finished) {
-        Exn.capture(server_socket.accept) match {
-          case Exn.Res(socket) =>
-            Isabelle_Thread.fork(name = "server_connection")
-              { using(Server.Connection(socket))(handle) }
-          case Exn.Exn(_) => finished = true
-        }
-      }
-    }
-
-  def start { server_thread }
-
-  def join { server_thread.join; shutdown() }
 }