class type in_record_channel =object
..end
An 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 End_of_file
when
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 input
method. The end of the record is indicated by an End_of_file
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 input_eor
raises
End_of_file
. After reading a non-empty channel, one can
do input_eor
after the last regular record, and the following
input_eor
raises End_of_file
.