--- 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 *)
--- 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 */
--- 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 -}