src/Pure/PIDE/byte_message.ML

--- a/src/Pure/PIDE/byte_message.ML	Tue Jun 21 16:03:00 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML	Tue Jun 21 22:17:11 2022 +0200
@@ -6,18 +6,20 @@
 
 signature BYTE_MESSAGE =
 sig
-  val write: BinIO.outstream -> string list -> unit
+  val write: BinIO.outstream -> Bytes.T list -> unit
   val write_yxml: BinIO.outstream -> XML.tree -> 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
-  val write_message: BinIO.outstream -> string list -> unit
+  val write_line: BinIO.outstream -> Bytes.T -> unit
+  val read: BinIO.instream -> int -> Bytes.T
+  val read_block: BinIO.instream -> int -> Bytes.T option * int
+  val read_line: BinIO.instream -> Bytes.T option
+  val write_message: BinIO.outstream -> Bytes.T list -> unit
+  val write_message_string: 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
+  val read_message: BinIO.instream -> Bytes.T list option
+  val read_message_string: BinIO.instream -> string list option
+  val write_line_message: BinIO.outstream -> Bytes.T -> unit
+  val read_line_message: BinIO.instream -> Bytes.T option
 end;
 
 structure Byte_Message: BYTE_MESSAGE =
@@ -25,45 +27,48 @@
 
 (* output operations *)
 
-val write = File.outputs;
+val write = List.app o Bytes.write_stream;
 
 fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
-fun write_line stream s = (write stream [s, "\n"]; flush stream);
+fun write_line stream bs = (write stream [bs, Bytes.newline]; flush stream);
 
 
 (* input operations *)
 
-fun read stream n = File.input_size n stream;
+fun read stream n = Bytes.read_stream n stream;
 
 fun read_block stream n =
   let
     val msg = read stream n;
-    val len = size msg;
+    val len = Bytes.length msg;
   in (if len = n then SOME msg else NONE, len) end;
 
 fun read_line stream =
   let
-    val result = trim_line o String.implode o rev;
-    fun read_body cs =
+    val result = SOME o Bytes.trim_line;
+    fun read_body bs =
       (case BinIO.input1 stream of
-        NONE => if null cs then NONE else SOME (result cs)
+        NONE => if Bytes.is_empty bs then NONE else result bs
       | SOME b =>
           (case Byte.byteToChar b of
-            #"\n" => SOME (result cs)
-          | c => read_body (c :: cs)));
-  in read_body [] end;
+            #"\n" => result bs
+          | c => read_body (Bytes.add (str c) bs)));
+  in read_body Bytes.empty end;
 
 
 (* messages with multiple chunks (arbitrary content) *)
 
 fun make_header ns =
-  [space_implode "," (map Value.print_int ns), "\n"];
+  [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline];
 
 fun write_message stream chunks =
-  (write stream (make_header (map size chunks) @ chunks); flush stream);
+  (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream);
+
+fun write_message_string stream =
+  write_message stream o map Bytes.string;
 
 fun write_message_yxml stream chunks =
   (write stream (make_header (map YXML.body_size chunks));
@@ -82,26 +87,32 @@
         string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
 
 fun read_message stream =
-  read_line stream |> Option.map (parse_header #> map (read_chunk stream));
+  read_line stream |> Option.map (Bytes.content #> parse_header #> map (read_chunk stream));
+
+fun read_message_string stream =
+  read_message stream |> (Option.map o map) Bytes.content;
 
 
 (* hybrid messages: line or length+block (with content restriction) *)
 
+(* line message format *)
+
 fun is_length msg =
-  msg <> "" andalso forall_string Symbol.is_ascii_digit msg;
+  not (Bytes.is_empty msg) andalso Bytes.forall_string Symbol.is_ascii_digit msg;
 
 fun is_terminated msg =
-  let val len = size msg
-  in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end;
+  (case Bytes.last_string msg of
+    NONE => false
+  | SOME s => Symbol.is_ascii_line_terminator s);
 
 fun write_line_message stream msg =
   if is_length msg orelse is_terminated msg then
-    error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
+    error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg)
   else
-    let val n = size msg in
+    let val n = Bytes.length msg in
       write stream
-        ((if n > 100 orelse exists_string (fn s => s = "\n") msg
-          then make_header [n + 1] else []) @ [msg, "\n"]);
+        ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg
+          then make_header [n + 1] else []) @ [msg, Bytes.newline]);
       flush stream
     end;
 
@@ -109,8 +120,8 @@
   (case read_line stream of
     NONE => NONE
   | SOME line =>
-      (case try Value.parse_nat line of
+      (case try (Value.parse_nat o Bytes.content) line of
         NONE => SOME line
-      | SOME n => Option.map trim_line (#1 (read_block stream n))));
+      | SOME n => Option.map Bytes.trim_line (#1 (read_block stream n))));
 
 end;