--- a/src/Tools/Haskell/Haskell.thy Mon Dec 10 23:36:29 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Tue Dec 11 19:25:35 2018 +0100
@@ -1368,15 +1368,18 @@
\([], a) -> App (pair term term a)]
\<close>
-generate_file "Isabelle/Bytes.hs" = \<open>
-{- Title: Isabelle/Bytes.hs
+generate_file "Isabelle/Byte_Message.hs" = \<open>
+{- Title: Isabelle/Byte_Message.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
-Byte-vector messages.
+Byte-oriented messages.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
-}
-module Isabelle.Bytes (read_line, read_block, read_message, write_message)
+module Isabelle.Byte_Message (read_line, read_block, trim_line, read_line_message, write_line_message)
where
import Data.ByteString (ByteString)
@@ -1384,6 +1387,7 @@
import qualified Data.ByteString.UTF8 as UTF8
import Data.Word (Word8)
+import Control.Monad (when)
import Network.Socket (Socket)
import qualified Network.Socket as Socket
import qualified Network.Socket.ByteString as ByteString
@@ -1391,8 +1395,6 @@
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
@@ -1411,13 +1413,15 @@
10 -> return (Just (result bs))
b -> read (b : bs)
-read_block :: Socket -> Int -> IO ByteString
+read_block :: Socket -> Int -> IO (Maybe ByteString)
read_block socket n = read 0 []
where
- result :: [ByteString] -> ByteString
- result = ByteString.concat . reverse
+ 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 ByteString
+ read :: Int -> [ByteString] -> IO (Maybe ByteString)
read len ss =
if len >= n then return (result ss)
else
@@ -1427,27 +1431,48 @@
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
+ else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
+ else s
+ where
+ n = ByteString.length s
+ at = ByteString.index s
--- see also \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
+
+
+-- hybrid messages: line or length+block (with content restriction)
+
+is_length :: ByteString -> Bool
+is_length s =
+ not (ByteString.null s) && ByteString.all (\b -> 48 <= b && b <= 57) s
-read_message :: Socket -> IO (Maybe ByteString)
-read_message socket = do
+has_line_terminator :: ByteString -> Bool
+has_line_terminator s =
+ not (ByteString.null s) && (ByteString.last s == 13 || ByteString.last s == 10)
+
+write_line_message :: Socket -> ByteString -> IO ()
+write_line_message socket msg = do
+ when (is_length msg || has_line_terminator msg) $
+ error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
+
+ 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])
+
+read_line_message :: Socket -> IO (Maybe ByteString)
+read_line_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])
+ Just n -> fmap trim_line <$> read_block socket n
\<close>
end