src/Tools/Haskell/Haskell.thy

 -}
 
 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
 
 import Prelude hiding (read)
 import Data.Maybe

 
 make_header :: [Int] -> [ByteString]
 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 =
   let
     res = map Value.parse_nat (space_explode ',' (UTF8.toString line))

 
 is_terminated :: ByteString -> Bool
 is_terminated msg =
   not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10)
 
+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]
+
 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))
-
-  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 = write socket . make_line_message
 
 read_line_message :: Socket -> IO (Maybe ByteString)
 read_line_message socket = do
   opt_line <- read_line socket
   case opt_line of