# HG changeset patch
# User wenzelm
# Date 1544632469 -3600
# Node ID ef051edd4d10b2cd971e8eac0a856859a9b47714
# Parent  dcea1fffbfe6e3597522364f14f9c096cfa02e37
more uniform multi-language operations;
misc tuning and clarification;

diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Dec 12 14:19:56 2018 +0100
+++ b/src/Pure/General/bytes.scala	Wed Dec 12 17:34:29 2018 +0100
@@ -39,6 +39,7 @@
       new Bytes(b, 0, b.length)
     }
 
+  val newline: Bytes = apply("\n")
 
   def base64(s: String): Bytes =
   {
diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML	Wed Dec 12 14:19:56 2018 +0100
+++ b/src/Pure/PIDE/byte_message.ML	Wed Dec 12 17:34:29 2018 +0100
@@ -6,20 +6,13 @@
 
 signature BYTE_MESSAGE =
 sig
-  val write: BinIO.outstream -> string -> unit
+  val write: BinIO.outstream -> string list -> unit
   val flush: BinIO.outstream -> 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_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;
@@ -29,9 +22,7 @@
 
 (* output operations *)
 
-fun write stream s = BinIO.output (stream, Byte.stringToBytes s);
-
-fun newline stream = write stream "\n";
+fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s));
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
@@ -59,35 +50,17 @@
   in read_body [] end;
 
 
-(* header with chunk lengths *)
+(* messages with multiple chunks (arbitrary content) *)
 
-fun write_header stream ns =
- (write stream (space_implode "," (map string_of_int ns));
-  newline stream);
+fun make_header stream ns =
+  [space_implode "," (map Value.print_int ns), "\n"];
 
-fun err_header line =
-  error ("Malformed message header: " ^ quote line);
+fun write_message stream chunks =
+  (write stream (make_header stream (map size chunks) @ chunks); flush stream);
 
 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);
+    handle Fail _ => error ("Malformed message header: " ^ quote line);
 
 fun read_chunk stream n =
   (case read_block stream n of
@@ -97,7 +70,7 @@
         string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
 
 fun read_message stream =
-  read_header stream |> (Option.map o map) (read_chunk stream);
+  read_line stream |> Option.map (parse_header #> map (read_chunk stream));
 
 
 (* hybrid messages: line or length+block (with content restriction) *)
@@ -114,10 +87,9 @@
     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;
+      write stream
+        ((if n > 100 orelse exists_string (fn s => s = "\n") msg
+          then make_header stream [n + 1] else []) @ [msg, "\n"]);
       flush stream
     end;
 
diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Wed Dec 12 14:19:56 2018 +0100
+++ b/src/Pure/PIDE/byte_message.scala	Wed Dec 12 17:34:29 2018 +0100
@@ -13,9 +13,8 @@
 {
   /* output operations */
 
-  def write(stream: OutputStream, bytes: Bytes) { bytes.write_stream(stream) }
-
-  def newline(stream: OutputStream) { stream.write(10) }
+  def write(stream: OutputStream, bytes: List[Bytes]): Unit =
+    bytes.foreach(_.write_stream(stream))
 
   def flush(stream: OutputStream): Unit =
     try { stream.flush() }
@@ -50,40 +49,20 @@
   }
 
 
-  /* header with chunk lengths */
+  /* messages with multiple chunks (arbitrary content) */
 
-  def write_header(stream: OutputStream, ns: List[Int])
+  private def make_header(ns: List[Int]): List[Bytes] =
+    List(Bytes(ns.mkString(",")), Bytes.newline)
+
+  def write_message(stream: OutputStream, chunks: List[Bytes])
   {
-    stream.write(UTF8.bytes(ns.mkString(",")))
-    newline(stream)
+    write(stream, make_header(chunks.map(_.length)) ::: chunks)
+    flush(stream)
   }
 
-  private def err_header(line: String): Nothing =
-    error("Malformed message header: " + quote(line))
-
   private def parse_header(line: String): List[Int] =
     try { space_explode(',', line).map(Value.Nat.parse) }
-    catch { case ERROR(_) => err_header(line) }
-
-  def read_header(stream: InputStream): Option[List[Int]] =
-    read_line(stream).map(_.text).map(parse_header(_))
-
-  def read_header1(stream: InputStream): Option[Int] =
-    read_line(stream).map(_.text).map(line =>
-      parse_header(line) match {
-        case List(n) => n
-        case _ => err_header(line)
-      })
-
-
-  /* messages with multiple chunks (arbitrary content) */
-
-  def write_message(stream: OutputStream, chunks: List[Bytes])
-  {
-    write_header(stream, chunks.map(_.length))
-    chunks.foreach(write(stream, _))
-    flush(stream)
-  }
+    catch { case ERROR(_) => error("Malformed message header: " + quote(line)) }
 
   private def read_chunk(stream: InputStream, n: Int): Bytes =
     read_block(stream, n) match {
@@ -93,7 +72,7 @@
     }
 
   def read_message(stream: InputStream): Option[List[Bytes]] =
-    read_header(stream).map(ns => ns.map(n => read_chunk(stream, n)))
+    read_line(stream).map(line => parse_header(line.text).map(read_chunk(stream, _)))
 
 
   /* hybrid messages: line or length+block (restricted content) */
@@ -113,10 +92,9 @@
       error ("Bad content for line message:\n" ++ msg.text.take(100))
 
     val n = msg.length
-    if (n > 100 || msg.iterator.contains(10)) write_header(stream, List(n + 1))
-
-    write(stream, msg)
-    newline(stream)
+    write(stream,
+      (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
+        List(msg, Bytes.newline))
     flush(stream)
   }
 
diff -r dcea1fffbfe6 -r ef051edd4d10 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Dec 12 14:19:56 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Dec 12 17:34:29 2018 +0100
@@ -1409,13 +1409,14 @@
 -}
 
 module Isabelle.Byte_Message (
-    write, newline,
-    read, read_block, trim_line, read_line,
-    read_line_message, write_line_message
+    write, read, read_block, trim_line, read_line,
+    write_message, read_message,
+    write_line_message, read_line_message
   )
 where
 
 import Prelude hiding (read)
+import Data.Maybe
 import Data.ByteString (ByteString)
 import qualified Data.ByteString as ByteString
 import qualified Data.ByteString.UTF8 as UTF8
@@ -1426,6 +1427,7 @@
 import qualified Network.Socket as Socket
 import qualified Network.Socket.ByteString as ByteString
 
+import Isabelle.Library hiding (trim_line)
 import qualified Isabelle.Value as Value
 
 
@@ -1482,6 +1484,42 @@
             b -> read_body (b : bs)
 
 
+{- messages with multiple chunks (arbitrary content) -}
+
+make_header :: [Int] -> [ByteString]
+make_header ns =
+  [UTF8.fromString (space_implode "," (map Value.print_int ns)), newline]
+
+write_message :: Socket -> [ByteString] -> IO ()
+write_message socket chunks =
+  write socket (make_header (map ByteString.length chunks) ++ chunks)
+
+parse_header :: ByteString -> [Int]
+parse_header line =
+  let
+    res = map Value.parse_nat (space_explode ',' (UTF8.toString line))
+  in
+    if all isJust res then map fromJust res
+    else error ("Malformed message header: " ++ quote (UTF8.toString line))
+
+read_chunk :: Socket -> Int -> IO ByteString
+read_chunk socket n = do
+  res <- read_block socket n
+  return $
+    case res of
+      (Just chunk, _) -> chunk
+      (Nothing, len) ->
+        error ("Malformed message chunk: unexpected EOF after " ++
+          show len ++ " of " ++ show n ++ " bytes")
+
+read_message :: Socket -> IO (Maybe [ByteString])
+read_message socket = do
+  res <- read_line socket
+  case res of
+    Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
+    Nothing -> return Nothing
+
+
 -- hybrid messages: line or length+block (with content restriction)
 
 is_length :: ByteString -> Bool
@@ -1498,10 +1536,9 @@
     error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
 
   let n = ByteString.length msg
-  write socket
-    (if n > 100 || ByteString.any (== 10) msg then
-      [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline]
-     else [msg, newline])
+  write socket $
+    (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++
+    [msg, newline]
 
 read_line_message :: Socket -> IO (Maybe ByteString)
 read_line_message socket = do