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