note description: "Interface for character input streams" library: "Gobo Eiffel Kernel Library" copyright: "Copyright (c) 2001-2018, Eric Bezault and others" license: "MIT License" date: "$Date: 2019-02-07 22:54:15 +0000 (Thu, 07 Feb 2019) $" revision: "$Revision: 102807 $" deferred class interface KI_CHARACTER_INPUT_STREAM feature -- Input read_string (nb: INTEGER_32) -- Read at most nb characters from input stream. -- Make the characters that have actually been read -- available in last_string. -- (Note that even if at least nb characters are available -- in the input stream, there is no guarantee that they -- will all be read.) require is_open_read: is_open_read not_end_of_input: not end_of_input nb_large_enough: nb > 0 ensure last_string_count_small_enough: not end_of_input implies last_string.count <= nb character_read: not end_of_input implies last_string.count > 0 read_to_string (a_string: STRING_8; pos, nb: INTEGER_32): INTEGER_32 -- Fill a_string, starting at position pos, with -- at most nb characters read from input stream. -- Return the number of characters actually read. -- (Note that even if at least nb characters are available -- in the input stream, there is no guarantee that they -- will all be read.) require is_open_read: is_open_read not_end_of_input: not end_of_input a_string_not_void: a_string /= Void valid_position: a_string.valid_index (pos) nb_large_enough: nb > 0 nb_small_enough: nb <= a_string.count - pos + 1 ensure nb_char_read_large_enough: Result >= 0 nb_char_read_small_enough: Result <= nb character_read: not end_of_input implies Result > 0 feature -- Access last_string: STRING_8 -- Last string read -- (Note: this query always return the same object. -- Therefore a clone should be used if the result -- is to be kept beyond the next call to this feature. -- However last_string is not shared between file objects.) require is_open_read: is_open_read not_end_of_input: not end_of_input ensure last_string_not_void: Result /= Void string_type: Any_.same_types (Result, "") feature -- Status report valid_unread_character (a_character: CHARACTER_8): BOOLEAN -- Can a_character be put back in input stream? end -- class KI_CHARACTER_INPUT_STREAM
Generated by ISE EiffelStudio