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