# HG changeset patch
# User wenzelm
# Date 1544733369 -3600
# Node ID e8893c8932410c0c5230875bd9a23aaf3e8c387c
# Parent  796e01aba901617f3a650511c6452d2e77a3f8db
tuned signature;

diff -r 796e01aba901 -r e8893c893241 src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML	Thu Dec 13 21:23:39 2018 +0100
+++ b/src/Pure/PIDE/byte_message.ML	Thu Dec 13 21:36:09 2018 +0100
@@ -8,6 +8,7 @@
 sig
   val write: BinIO.outstream -> string list -> unit
   val flush: BinIO.outstream -> unit
+  val write_line: BinIO.outstream -> string -> unit
   val read: BinIO.instream -> int -> string
   val read_block: BinIO.instream -> int -> string option * int
   val read_line: BinIO.instream -> string option
@@ -26,6 +27,8 @@
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
+fun write_line stream s = (write stream [s, "\n"]; flush stream);
+
 
 (* input operations *)
 
diff -r 796e01aba901 -r e8893c893241 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 */
 
diff -r 796e01aba901 -r e8893c893241 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Dec 13 21:23:39 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 13 21:36:09 2018 +0100
@@ -1467,7 +1467,8 @@
 -}
 
 module Isabelle.Byte_Message (
-    write, read, read_block, trim_line, read_line,
+    write, write_line,
+    read, read_block, trim_line, read_line,
     write_message, read_message,
     write_line_message, read_line_message
   )
@@ -1497,6 +1498,9 @@
 newline :: ByteString
 newline = ByteString.singleton 10
 
+write_line :: Socket -> ByteString -> IO ()
+write_line socket s = write socket [s, newline]
+
 
 {- input operations -}