src/Pure/PIDE/byte_message.ML

--- a/src/Pure/PIDE/byte_message.ML	Tue Dec 11 23:59:41 2018 +0100
+++ b/src/Pure/PIDE/byte_message.ML	Wed Dec 12 00:01:11 2018 +0100
@@ -6,15 +6,38 @@
 
 signature BYTE_MESSAGE =
 sig
-  val read_line: BinIO.instream -> string option
+  val write: BinIO.outstream -> string -> unit
+  val newline: BinIO.outstream -> unit
+  val flush: BinIO.outstream -> unit
   val read: BinIO.instream -> int -> string
   val read_block: BinIO.instream -> int -> string option
+  val read_line: BinIO.instream -> string option
+
+  val write_header: BinIO.outstream -> int list -> unit
+  val read_header: BinIO.instream -> int list option
+  val read_header1: BinIO.instream -> int option
+
+  val write_message: BinIO.outstream -> string 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
 end;
 
 structure Byte_Message: BYTE_MESSAGE =
 struct
 
+(* output operations *)
+
+fun write stream s = BinIO.output (stream, Byte.stringToBytes s);
+
+fun newline stream = write stream "\n";
+
+fun flush stream = ignore (try BinIO.flushOut stream);
+
+
+(* input operations *)
+
 fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
 
 fun read_block stream n =
@@ -34,10 +57,40 @@
   in read [] end;
 
 
+(* header with chunk lengths *)
+
+fun write_header stream ns =
+ (write stream (space_implode "," (map string_of_int ns));
+  newline stream);
+
+fun err_header line = error ("Malformed message header: " ^ quote line)
+
+fun parse_header line =
+  map Value.parse_nat (space_explode "," line)
+    handle Fail _ => err_header line
+
+fun read_header stream =
+  read_line stream |> Option.map parse_header;
+
+fun read_header1 stream =
+  read_line stream |> Option.map (fn line =>
+    (case parse_header line of
+      [n] => n
+    | _ => err_header line));
+
+
 (* messages with multiple chunks (arbitrary content) *)
 
+fun write_message stream chunks =
+ (write_header stream (map size chunks);
+  List.app (write stream) chunks;
+  flush stream);
+
 fun read_chunk stream n =
-  let val (len, chunk) = `size (read stream n) in
+  let
+    val chunk = read stream n;
+    val len = size chunk;
+  in
     if len = n then chunk
     else
       error ("Malformed message chunk: unexpected EOF after " ^
@@ -45,10 +98,36 @@
   end;
 
 fun read_message stream =
-  read_line stream |> Option.map (fn line =>
-    let
-      val ns = map Value.parse_nat (space_explode "," line)
-        handle Fail _ => error ("Malformed message header: " ^ quote line);
-    in map (read_chunk stream) ns end);
+  read_header stream |> (Option.map o map) (read_chunk stream);
+
+
+(* hybrid messages: line or length+block (with content restriction) *)
+
+fun is_length s =
+  s <> "" andalso forall_string Symbol.is_ascii_digit s;
+
+fun has_line_terminator s =
+  String.isSuffix "\r" s orelse String.isSuffix "\n" s;
+
+fun write_line_message stream msg =
+  if is_length msg orelse has_line_terminator msg then
+    error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
+  else
+    let val n = size msg in
+      if n > 100 orelse exists_string (fn s => s = "\n") msg then
+        write_header stream [n + 1]
+      else ();
+      write stream msg;
+      newline stream;
+      flush stream
+    end;
+
+fun read_line_message stream =
+  (case read_line stream of
+    SOME line =>
+      (case try Value.parse_nat line of
+        NONE => SOME line
+      | SOME n => Option.map trim_line (read_block stream n))
+  | NONE => NONE) handle IO.Io _ => NONE;
 
 end;