--- a/src/Pure/Tools/server.scala Thu Aug 12 13:14:49 2021 +0200
+++ b/src/Pure/Tools/server.scala Thu Aug 12 13:19:56 2021 +0200
@@ -128,6 +128,7 @@
{
val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
def port: Int = socket.getLocalPort
+ def address: String = print_address(port)
val password: String = UUID.random().toString
override def toString: String = print(port, password)
@@ -189,6 +190,10 @@
try { Byte_Message.read_line_message(in).map(_.text) }
catch { case _: IOException => None }
+ def read_byte_message(): Option[List[Bytes]] =
+ try { Byte_Message.read_message(in) }
+ catch { case _: IOException => None }
+
def await_close(): Unit =
try { Byte_Message.read(in, 1); socket.close() }
catch { case _: IOException => }
@@ -196,6 +201,9 @@
def write_line_message(msg: String): Unit =
out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
+ def write_byte_message(chunks: List[Bytes]): Unit =
+ out_lock.synchronized { Byte_Message.write_message(out, chunks) }
+
def reply(r: Reply.Value, arg: Any): Unit =
{
val argument = Argument.print(arg)