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