# 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)