--- a/src/Tools/Haskell/Haskell.thy Tue Aug 24 17:35:29 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Tue Aug 24 20:25:53 2021 +0200
@@ -1208,8 +1208,7 @@
start, none, put_file, file, file_only, put_id, id, id_only,
symbol, symbol_explode, symbol_explode_string, shift_offsets,
of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
- is_reported, is_reported_range, here,
-
+ Report, Report_Text, is_reported, is_reported_range, here,
Range, no_range, no_range_position, range_position, range
)
where
@@ -1380,6 +1379,9 @@
{- reports -}
+type Report = (T, Markup.T)
+type Report_Text = (Report, Bytes)
+
is_reported :: T -> Bool
is_reported pos = isJust (offset_of pos) && isJust (id_of pos)
@@ -2735,7 +2737,8 @@
module Isabelle.Byte_Message (
write, write_line,
read, read_block, read_line,
- make_message, write_message, read_message, exchange_message,
+ make_message, write_message, read_message,
+ exchange_message, exchange_message0,
make_line_message, write_line_message, read_line_message,
read_yxml, write_yxml
)
@@ -2843,6 +2846,11 @@
write_message socket msg
read_message socket
+exchange_message0 :: Socket -> [Bytes] -> IO ()
+exchange_message0 socket msg = do
+ _ <- exchange_message socket msg
+ return ()
+
-- hybrid messages: line or length+block (with content restriction)