src/Pure/PIDE/byte_message.scala

--- a/src/Pure/PIDE/byte_message.scala	Thu Dec 13 21:23:39 2018 +0100
+++ b/src/Pure/PIDE/byte_message.scala	Thu Dec 13 21:36:09 2018 +0100
@@ -20,6 +20,12 @@
     try { stream.flush() }
     catch { case _: IOException => }
 
+  def write_line(stream: OutputStream, bytes: Bytes): Unit =
+  {
+    write(stream, List(bytes, Bytes.newline))
+    flush(stream)
+  }
+
 
   /* input operations */