# HG changeset patch # User wenzelm # Date 1520594996 -3600 # Node ID be6d69595ca76ed9e6a1232b56f404959651efcf # Parent ad96390ceb5d1922958a4ac856752ef3895df66a clarified socket connection; diff -r ad96390ceb5d -r be6d69595ca7 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Fri Mar 09 12:07:47 2018 +0100 +++ b/src/Pure/Tools/server.scala Fri Mar 09 12:29:56 2018 +0100 @@ -28,6 +28,49 @@ } + /* socket connection */ + + object Connection + { + def apply(socket: Socket): Connection = + new Connection(socket) + } + + class Connection private(socket: Socket) + { + override def toString: String = socket.toString + + def close() { socket.close } + + val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset)) + val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset)) + + def read_line(): Option[String] = + reader.readLine() match { + case null => None + case line => Some(line) + } + + def write_line(msg: String) + { + require(split_lines(msg).length <= 1) + writer.write(msg) + writer.newLine() + writer.flush() + } + + def reply(r: Server.Reply.Value, t: JSON.T) + { + write_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t)) + } + + def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) } + def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) } + def reply_error_message(message: String, more: (String, JSON.T)*): Unit = + reply_error(Map("message" -> message) ++ more) + } + + /* per-user servers */ object Data @@ -44,11 +87,11 @@ def print: String = "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")" - def connect(): Socket = - new Socket(InetAddress.getByName("127.0.0.1"), port) + def connection(): Connection = + Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) def active(): Boolean = - try { connect().close; true } + try { connection().close; true } catch { case _: IOException => false } } } @@ -99,9 +142,10 @@ db.transaction { find(db, name) match { case Some(entry) => - using(entry.connect())(socket => + using(entry.connection())(connection => { - using(socket.getOutputStream)(_.write(UTF8.bytes(entry.password + "\nshutdown"))) + connection.write_line(entry.password) + connection.write_line("shutdown") }) while(entry.active) { Thread.sleep(100) } true @@ -156,59 +200,38 @@ private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1")) def port: Int = server_socket.getLocalPort - def shutdown() { server_socket.close } val password: String = Library.UUID() - private def handle_connection(socket: Socket) + private def handle(connection: Server.Connection) { - val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset)) - val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset)) - - def reply_line(msg: String) - { - require(split_lines(msg).length <= 1) - writer.write(msg) - writer.newLine() - writer.flush() - } - - def reply(r: Server.Reply.Value, t: JSON.T) - { - reply_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t)) - } - - def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) } - def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) } - def reply_error_message(message: String, more: (String, JSON.T)*): Unit = - reply_error(Map("message" -> message) ++ more) - - reader.readLine() match { - case null => - case bad if bad != password => reply_error("Bad password -- connection closed") + connection.read_line() match { + case None => + case Some(line) if line != password => + connection.reply_error("Bad password -- connection closed") case _ => var finished = false while (!finished) { - reader.readLine() match { - case null => finished = true - case line => + connection.read_line() match { + case None => finished = true + case Some(line) => val cmd = line.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c)) val input = line.substring(cmd.length).dropWhile(Symbol.is_ascii_blank(_)) Server.commands.get(cmd) match { - case None => reply_error("Bad command " + quote(cmd)) + case None => connection.reply_error("Bad command " + quote(cmd)) case Some(body) => proper_string(input) getOrElse "{}" match { case JSON.Format(arg) => if (body.isDefinedAt((server, arg))) { - try { reply_ok(body(server, arg)) } - catch { case ERROR(msg) => reply_error(msg) } + try { connection.reply_ok(body(server, arg)) } + catch { case ERROR(msg) => connection.reply_error(msg) } } else { - reply_error_message( + connection.reply_error_message( "Bad argument for command", "command" -> cmd, "argument" -> arg) } case _ => - reply_error_message( + connection.reply_error_message( "Malformed command-line", "command" -> cmd, "input" -> input) } } @@ -218,18 +241,20 @@ } } - private lazy val thread: Thread = + private lazy val server_thread: Thread = Standard_Thread.fork("server") { var finished = false while (!finished) { Exn.capture(server_socket.accept) match { case Exn.Res(socket) => Standard_Thread.fork("server_connection") - { try { handle_connection(socket) } finally { socket.close } } + { using(Server.Connection(socket))(handle(_)) } case Exn.Exn(_) => finished = true } } } - def join { thread.join; shutdown() } + def join { server_thread.join; shutdown() } + + def shutdown() { server_socket.close } }