--- a/src/Pure/PIDE/byte_message.ML Sun Apr 11 21:32:09 2021 +0200
+++ b/src/Pure/PIDE/byte_message.ML Sun Apr 11 22:47:55 2021 +0200
@@ -14,6 +14,7 @@
val read_block: BinIO.instream -> int -> string option * int
val read_line: BinIO.instream -> string option
val write_message: BinIO.outstream -> string list -> unit
+ val write_message_yxml: BinIO.outstream -> XML.body list -> unit
val read_message: BinIO.instream -> string list option
val write_line_message: BinIO.outstream -> string -> unit
val read_line_message: BinIO.instream -> string option
@@ -64,6 +65,11 @@
fun write_message stream chunks =
(write stream (make_header (map size chunks) @ chunks); flush stream);
+fun write_message_yxml stream chunks =
+ (write stream (make_header (map YXML.body_size chunks));
+ (List.app o List.app) (write_yxml stream) chunks;
+ flush stream);
+
fun parse_header line =
map Value.parse_nat (space_explode "," line)
handle Fail _ => error ("Malformed message header: " ^ quote line);