class type in_record_channel =
in_record_channelcan be used to read files with record structure. This is purely abstract, as Unix does not support such files natively, so this kind of channel is usually mapped to a flat representation when stored in a real file, e.g. record boundaries become newline characters.
method input_eor :
unit -> unit
End_of_filewhen the current record is the "EOF" record (see below for explanations).
A record channel can be read as follows: After opening the channel,
one can read the contents of the first record with the
method. The end of the record is indicated by an
exception. By calling
input_eor, the next record is opened
and can be read.
After the last real record, there is always a special
"EOF" record which is empty, and must be ignored by applications
processing records. This means, after opening an empty channel,
the current record is this "EOF" record, and
End_of_file. After reading a non-empty channel, one can
input_eor after the last regular record, and the following