# HG changeset patch # User wenzelm # Date 1629819329 -7200 # Node ID 92e74f9305a46513d6090af0a3c1051c8038e482 # Parent 2508ea6a9a11077435ac4b508ad0b034b0511513 more Isabelle/Haskell operations; diff -r 2508ea6a9a11 -r 92e74f9305a4 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Tue Aug 24 16:42:45 2021 +0200 +++ b/src/Tools/Haskell/Haskell.thy Tue Aug 24 17:35:29 2021 +0200 @@ -2735,7 +2735,7 @@ module Isabelle.Byte_Message ( write, write_line, read, read_block, read_line, - make_message, write_message, read_message, + make_message, write_message, read_message, exchange_message, make_line_message, write_line_message, read_line_message, read_yxml, write_yxml ) @@ -2838,6 +2838,11 @@ Just line -> Just <$> mapM (read_chunk socket) (parse_header line) Nothing -> return Nothing +exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes]) +exchange_message socket msg = do + write_message socket msg + read_message socket + -- hybrid messages: line or length+block (with content restriction)