# HG changeset patch
# User wenzelm
# Date 1628767196 -7200
# Node ID 608f8ae89cac8c83a9414bbeb14f8b56211f2707
# Parent  f9f6a31cc99c9e046ff82516b066c8d35a9e5bec
clarified signature;

diff -r f9f6a31cc99c -r 608f8ae89cac src/Pure/Tools/server.scala
--- 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)