note description: "Interface for 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_INPUT_STREAM [G] feature -- Input read -- Read the next item in input stream. -- Make the result available in last_item. require is_open_read: is_open_read not_end_of_input: not end_of_input unread (an_item: G) -- Put an_item back in input stream. -- This item will be read first by the next -- call to a read routine. require is_open_read: is_open_read an_item_valid: valid_unread_item (an_item) ensure not_end_of_input: not end_of_input last_item_set: last_item = an_item read_to_buffer (a_buffer: KI_BUFFER [G]; pos, nb: INTEGER_32): INTEGER_32 -- Fill a_buffer, starting at position pos, with -- at most nb items read from input stream. -- Return the number of items actually read. -- (Note that even if at least nb items 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_buffer_not_void: a_buffer /= Void pos_large_enough: pos >= 1 nb_large_enough: nb > 0 enough_space: (pos + nb - 1) <= a_buffer.count ensure nb_item_read_large_enough: Result >= 0 nb_item_read_small_enough: Result <= nb not_end_of_input: not end_of_input implies Result > 0 feature -- Status report is_closable: BOOLEAN -- Can current input stream be closed? ensure is_open: Result implies is_open_read is_open_read: BOOLEAN -- Can items be read from input stream? is_rewindable: BOOLEAN -- Can current input stream be rewound to return input from -- the beginning of the stream? ensure rewind_implies_open: Result implies is_open_read end_of_input: BOOLEAN -- Has the end of input stream been reached? require is_open_read: is_open_read valid_unread_item (an_item: G): BOOLEAN -- Can an_item be put back in input stream? feature -- Access name: STRING_8 -- Name of input stream ensure name_not_void: Result /= Void last_item: G -- Last item read require is_open_read: is_open_read not_end_of_input: not end_of_input feature -- Basic operations close -- Try to close input stream if it is closable. Set -- is_open_read to false if operation was successful. require is_closable: is_closable rewind -- Move input position to the beginning of stream. require can_rewind: is_rewindable end -- class KI_INPUT_STREAM
Generated by ISE EiffelStudio