--- a/src/Tools/Haskell/Haskell.thy Tue Dec 11 19:25:35 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Tue Dec 11 21:23:02 2018 +0100
@@ -1379,9 +1379,12 @@
and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
-}
-module Isabelle.Byte_Message (read_line, read_block, trim_line, read_line_message, write_line_message)
+module Isabelle.Byte_Message
+ (read, read_block, read_line, trim_line,
+ read_line_message, write_line_message)
where
+import Prelude hiding (read)
import Data.ByteString (ByteString)
import qualified Data.ByteString as ByteString
import qualified Data.ByteString.UTF8 as UTF8
@@ -1395,6 +1398,27 @@
import qualified Isabelle.Value as Value
+read :: Socket -> Int -> IO ByteString
+read socket n = read_bytes 0 []
+ where
+ result :: [ByteString] -> ByteString
+ result = ByteString.concat . reverse
+
+ read_bytes :: Int -> [ByteString] -> IO ByteString
+ read_bytes 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_bytes (len + m) (s : ss))
+
+read_block :: Socket -> Int -> IO (Maybe ByteString)
+read_block socket n = do
+ s <- read socket n
+ return (if ByteString.length s == n then Just s else Nothing)
+
read_line :: Socket -> IO (Maybe ByteString)
read_line socket = read []
where
@@ -1413,24 +1437,6 @@
10 -> return (Just (result bs))
b -> read (b : bs)
-read_block :: Socket -> Int -> IO (Maybe ByteString)
-read_block socket n = read 0 []
- where
- result :: [ByteString] -> Maybe ByteString
- result ss =
- if ByteString.length s == n then Just s else Nothing
- where s = ByteString.concat (reverse ss)
-
- read :: Int -> [ByteString] -> IO (Maybe 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))
-
trim_line :: ByteString -> ByteString
trim_line s =
if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
@@ -1441,7 +1447,6 @@
at = ByteString.index s
-
-- hybrid messages: line or length+block (with content restriction)
is_length :: ByteString -> Bool