src/Tools/Haskell/Haskell.thy

 module Isabelle.Position (
   T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
   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
 
 import Prelude hiding (id)

   in Markup.entity kind name |> Markup.properties props
 
 
 {- 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)
 
 is_reported_range :: T -> Bool
 is_reported_range pos = is_reported pos && isJust (end_offset_of pos)

 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
 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
   )
 where
 

 
 exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes])
 exchange_message socket msg = do
   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)
 
 is_length :: Bytes -> Bool