# HG changeset patch
# User wenzelm
# Date 1544481389 -3600
# Node ID 9cf0b79dfb7f0d5fb4048d72188efca307d862d9
# Parent  bff0011cdf42c2700cf798e24e581b1e53e789df
more Haskell operations;

diff -r bff0011cdf42 -r 9cf0b79dfb7f src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Mon Dec 10 23:19:37 2018 +0100
+++ b/src/Pure/General/bytes.ML	Mon Dec 10 23:36:29 2018 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/bytes.ML
     Author:     Makarius
 
-Immutable byte vectors as ML strings.
+Byte-vector messages.
 *)
 
 signature BYTES =
diff -r bff0011cdf42 -r 9cf0b79dfb7f src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Dec 10 23:19:37 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Dec 10 23:36:29 2018 +0100
@@ -1368,4 +1368,86 @@
     \([], a) -> App (pair term term a)]
 \<close>
 
+generate_file "Isabelle/Bytes.hs" = \<open>
+{-  Title:      Isabelle/Bytes.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Byte-vector messages.
+-}
+
+module Isabelle.Bytes (read_line, read_block, read_message, write_message)
+where
+
+import Data.ByteString (ByteString)
+import qualified Data.ByteString as ByteString
+import qualified Data.ByteString.UTF8 as UTF8
+import Data.Word (Word8)
+
+import Network.Socket (Socket)
+import qualified Network.Socket as Socket
+import qualified Network.Socket.ByteString as ByteString
+
+import qualified Isabelle.Value as Value
+
+
+-- see also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/bytes.ML\<close>
+
+read_line :: Socket -> IO (Maybe ByteString)
+read_line socket = read []
+  where
+    result :: [Word8] -> ByteString
+    result bs =
+      ByteString.pack $ reverse $
+        if not (null bs) && head bs == 13 then tail bs else bs
+
+    read :: [Word8] -> IO (Maybe ByteString)
+    read bs = do
+      s <- ByteString.recv socket 1
+      case ByteString.length s of
+        0 -> return (if null bs then Nothing else Just (result bs))
+        1 ->
+          case ByteString.head s of
+            10 -> return (Just (result bs))
+            b -> read (b : bs)
+
+read_block :: Socket -> Int -> IO ByteString
+read_block socket n = read 0 []
+  where
+    result :: [ByteString] -> ByteString
+    result = ByteString.concat . reverse
+
+    read :: Int -> [ByteString] -> IO ByteString
+    read len ss =
+      if len >= n then return (result ss)
+      else
+        (do
+          s <- ByteString.recv socket (min (n - len) 8192)
+          case ByteString.length s of
+            0 -> return (result ss)
+            m -> read (len + m) (s : ss))
+
+
+-- see also \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
+
+read_message :: Socket -> IO (Maybe ByteString)
+read_message socket = do
+  opt_line <- read_line socket
+  case opt_line of
+    Nothing -> return Nothing
+    Just line ->
+      case Value.parse_int (UTF8.toString line) of
+        Nothing -> return $ Just line
+        Just n -> Just <$> read_block socket n
+
+write_message :: Socket -> ByteString -> IO ()
+write_message socket msg = do
+  let newline = ByteString.singleton 10
+  let n = ByteString.length msg
+  ByteString.sendMany socket
+    (if n > 100 || ByteString.any (== 10) msg then
+      [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline]
+     else [msg, newline])
+\<close>
+
 end
diff -r bff0011cdf42 -r 9cf0b79dfb7f src/Tools/Haskell/Test.thy
--- a/src/Tools/Haskell/Test.thy	Mon Dec 10 23:19:37 2018 +0100
+++ b/src/Tools/Haskell/Test.thy	Mon Dec 10 23:36:29 2018 +0100
@@ -15,7 +15,9 @@
 
       val modules = files
         |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
-      val _ = GHC.new_project tmp_dir {name = "isabelle", depends = [], modules = modules};
+      val _ =
+        GHC.new_project tmp_dir
+          {name = "isabelle", depends = ["bytestring", "utf8-string", "network"], modules = modules};
 
       val (out, rc) =
         Isabelle_System.bash_output