# HG changeset patch
# User wenzelm
# Date 1544967252 -3600
# Node ID d93fe3557a98ff1cef9f5681ab13c1a15a8f785b
# Parent  b3628ee55f28e17a2c446b1c36ee4cd32927e89e
clarified signature;

diff -r b3628ee55f28 -r d93fe3557a98 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Dec 16 13:24:24 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Sun Dec 16 14:34:12 2018 +0100
@@ -1471,8 +1471,8 @@
 module Isabelle.Byte_Message (
     write, write_line,
     read, read_block, trim_line, read_line,
-    write_message, read_message,
-    write_line_message, read_line_message
+    make_message, write_message, read_message,
+    make_line_message, write_line_message, read_line_message
   )
 where
 
@@ -1554,9 +1554,11 @@
 make_header ns =
   [UTF8.fromString (space_implode "," (map Value.print_int ns)), newline]
 
+make_message :: [ByteString] -> [ByteString]
+make_message chunks = make_header (map ByteString.length chunks) ++ chunks
+
 write_message :: Socket -> [ByteString] -> IO ()
-write_message socket chunks =
-  write socket (make_header (map ByteString.length chunks) ++ chunks)
+write_message socket = write socket . make_message
 
 parse_header :: ByteString -> [Int]
 parse_header line =
@@ -1594,15 +1596,17 @@
 is_terminated msg =
   not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10)
 
-write_line_message :: Socket -> ByteString -> IO ()
-write_line_message socket msg = do
-  when (is_length msg || is_terminated msg) $
-    error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
+make_line_message :: ByteString -> [ByteString]
+make_line_message msg =
+  let n = ByteString.length msg in
+    if is_length msg || is_terminated msg then
+      error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
+    else
+      (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++
+      [msg, newline]
 
-  let n = ByteString.length msg
-  write socket $
-    (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++
-    [msg, newline]
+write_line_message :: Socket -> ByteString -> IO ()
+write_line_message socket = write socket . make_line_message
 
 read_line_message :: Socket -> IO (Maybe ByteString)
 read_line_message socket = do