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 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 deferred end 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) deferred ensure not_end_of_input: not end_of_input last_item_set: last_item = an_item end 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 local i, end_pos: INTEGER_32 do end_pos := pos + nb - 1 from i := pos until i > end_pos loop read if not end_of_input then a_buffer.put (last_item, i) i := i + 1 else Result := i - pos - nb i := end_pos + 1 end end Result := Result + i - pos 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 end feature -- Status report is_closable: BOOLEAN -- Can current input stream be closed? do Result := False ensure is_open: Result implies is_open_read end is_open_read: BOOLEAN -- Can items be read from input stream? deferred end is_rewindable: BOOLEAN -- Can current input stream be rewound to return input from -- the beginning of the stream? do Result := False ensure rewind_implies_open: Result implies is_open_read end end_of_input: BOOLEAN -- Has the end of input stream been reached? require is_open_read: is_open_read deferred end valid_unread_item (an_item: G): BOOLEAN -- Can an_item be put back in input stream? deferred end feature -- Access name: STRING_8 -- Name of input stream deferred ensure name_not_void: Result /= Void end last_item: G -- Last item read require is_open_read: is_open_read not_end_of_input: not end_of_input deferred end 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 do end rewind -- Move input position to the beginning of stream. require can_rewind: is_rewindable do end end -- class KI_INPUT_STREAM
Generated by ISE EiffelStudio