indexing
	description: "Routines that ought to be in class INPUT_STREAM"
	library: "Gobo Eiffel Kernel Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

class interface
	KL_INPUT_STREAM_ROUTINES

feature -- Initialization

	make_file_open_read (a_filename: STRING): like input_stream_type
			-- Create a new file object with a_filename as
			-- file name and try to open it in read-only mode.
			-- is_open_read (Result) is set to True
			-- if operation was successful.
		require
			a_filename_not_void: a_filename /= void;
			a_filename_not_empty: not a_filename.empty
		ensure
			file_not_void: Result /= void
	
feature -- Access

	input_stream_: KL_INPUT_STREAM_ROUTINES
			-- Routines that ought to be in class INPUT_STREAM
			-- (from KL_IMPORTED_INPUT_STREAM_ROUTINES)
		ensure -- from KL_IMPORTED_INPUT_STREAM_ROUTINES
			input_stream_routines_not_void: Result /= void

	name (a_stream: like input_stream_type): STRING
			-- Name of a_stream
		require
			a_stream_void: a_stream /= void
		ensure
			name_not_void: Result /= void
	
feature -- Status report

	end_of_input (a_stream: like input_stream_type): BOOLEAN
			-- Has an EOF been detected?
		require
			a_stream_void: a_stream /= void;
			a_stream_is_open_read: is_open_read (a_stream)

	is_closed (a_stream: like input_stream_type): BOOLEAN
			-- Is a_stream closed?
		require
			a_stream_void: a_stream /= void

	is_open_read (a_stream: like input_stream_type): BOOLEAN
			-- Is a_stream open in read mode?
		require
			a_stream_void: a_stream /= void
	
feature -- Status setting

	close (a_stream: like input_stream_type)
			-- Close a_stream if it is closable,
			-- let it open otherwise.
		require
			a_stream_not_void: a_stream /= void;
			not_closed: not is_closed (a_stream)
	
feature -- Input operations

	read_stream (a_stream: like input_stream_type; a_buffer: STRING; pos, nb_char: INTEGER): INTEGER
			-- Fill a_buffer, starting at position pos with
			-- at most nb_char characters read from a_stream.
			-- Return the number of characters actually read.
		require
			a_stream_not_void: a_stream /= void;
			a_stream_open_read: is_open_read (a_stream);
			a_buffer_not_void: a_buffer /= void;
			valid_position: a_buffer.valid_index (pos);
			nb_char_large_enough: nb_char >= 0;
			nb_char_small_enough: nb_char <= a_buffer.count - pos + 1
		ensure
			nb_char_read_large_enough: Result >= 0;
			nb_char_read_small_enough: Result <= nb_char

	read_string (a_stream: like input_stream_type; nb_char: INTEGER): STRING
			-- Read at most nb_char characters read from a_stream.
			-- Return the characters that have actually been read.
		require
			a_stream_not_void: a_stream /= void;
			a_stream_open_read: is_open_read (a_stream);
			nb_char_large_enough: nb_char >= 0
		ensure
			string_not_void: Result /= void;
			string_count_small_enough: Result.count <= nb_char
	
feature -- Type anchors

	input_stream_type: IO_MEDIUM
			-- (from KL_IMPORTED_INPUT_STREAM_ROUTINES)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);

end -- class KL_INPUT_STREAM_ROUTINES