class type in_record_channel =
in_record_channel can 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
Skips over the remaining data of the current record and the
record boundary to the next record. Raises
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