Information for a file for reopening

The abstract type for an input buffer.

Type of fixed data attached to the buffer (like file name)

return the infos associated to a buffer

dummy infos

returns the stream_infos stored in infos

returns the filename if it exists, the empty string otherwise

utf8 infos return the unicode context in use for this file

The abstract type position relative to the current buffer

position at the beginning of a buffer

The abstract position relative to the beginning of buffer

convert byte_pos to natural number

zero

dummy value, to initiaize references for instance

Short (and quick) type for positions

dummy value, to initiaize references for instance

read buf idx returns the character at position idx in the buffer buf, together with the new buffer and position. Read infinitely many '\255' at end of buffer

sub b i len returns len characters from position idx. If the end of buffer is reached, the string is filed with eof '\255'

get buf idx returns the character at position idx in the buffer buf.

from_file fn returns a buffer constructed using the file fn.

If utf8 is Utf8.UTF8 or Utf8.CJK_UTF8 (Utf8.ASCII is the default), positions are reported according to utf8. read is still reading bytes.

Getting line number and column number requires rescanning the file and if the file is not a regular file, it is kept in memory. Setting rescan to false avoid this, but only byte position and file name will be available.

from_channel ~filename ch returns a buffer constructed using the channel ch. The optional filename is only used as a reference to the channel in error messages.

uft8 and rescan as in from_file.

Same as above for file descriptor

from_string ~filename str returns a buffer constructed using the string str. The optional filename is only used as a reference to the channel in error messages.

is_empty buf test whether the buffer buf is empty.

position in bytes, regardless to utf8

get spos from buffer and idx, to get line_num and col_num if needed later.

buffer_uid buf returns a unique identifier. Input.read does not change the uid. The uid is created when creating the initial buffer.

buffer_eq b1 b2 tests the equality of b1 and b2.

buffer_compare b1 b2 compares b1 and b2.

buffer_before b1 i1 b2 i2 returns true if the position b1, i1 is before b2, i2. Gives meaningless result if b1 and b2 do not refer to the same file, i.e. do not have the same uid.

Table to associate value to positions in input buffers. The complexity of access in the table is O(ln(N)) where N is the number of tables.