diff -r 12c984b7d391 -r 6d8674ffb962 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Fri Jul 30 22:54:50 2021 +0200 +++ b/src/Tools/Haskell/Haskell.thy Fri Jul 30 23:00:50 2021 +0200 @@ -23,7 +23,7 @@ Bytes, make, unmake, pack, unpack, empty, null, length, index, all, any, - head, last, take, drop, concat, + head, last, take, drop, concat, trim_line ) where @@ -82,6 +82,15 @@ concat :: [Bytes] -> Bytes concat = mconcat + +trim_line :: Bytes -> Bytes +trim_line s = + if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then take (n - 2) s + else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then take (n - 1) s + else s + where + n = length s + at = index s \ generate_file "Isabelle/UTF8.hs" = \ @@ -1840,7 +1849,7 @@ module Isabelle.Byte_Message ( write, write_line, - read, read_block, trim_line, read_line, + read, read_block, read_line, make_message, write_message, read_message, make_line_message, write_line_message, read_line_message, read_yxml, write_yxml @@ -1859,7 +1868,7 @@ import Network.Socket (Socket) import qualified Network.Socket.ByteString as Socket -import Isabelle.Library hiding (trim_line) +import Isabelle.Library import qualified Isabelle.Value as Value @@ -1893,19 +1902,10 @@ let len = Bytes.length msg return (if len == n then Just msg else Nothing, len) -trim_line :: Bytes -> Bytes -trim_line s = - if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then Bytes.take (n - 2) s - else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then Bytes.take (n - 1) s - else s - where - n = Bytes.length s - at = Bytes.index s - read_line :: Socket -> IO (Maybe Bytes) read_line socket = read_body [] where - result = trim_line . Bytes.pack . reverse + result = Bytes.trim_line . Bytes.pack . reverse read_body bs = do s <- Socket.recv socket 1 case ByteString.length s of @@ -1982,7 +1982,7 @@ Just line -> case Value.parse_nat (UTF8.decode line) of Nothing -> return $ Just line - Just n -> fmap trim_line . fst <$> read_block socket n + Just n -> fmap Bytes.trim_line . fst <$> read_block socket n read_yxml :: Socket -> IO (Maybe XML.Body)