indexing
	description: "Routines that ought to be in class STRING_BUFFER. A string buffer is a sequence of characters equipped with features `put%', `item%' and `count%'."
	library: "Gobo Eiffel Kernel Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1999, Eric Bezault"

class interface
	KL_STRING_BUFFER_ROUTINES

feature -- Initialization

	make (n: INTEGER): like string_buffer_type
			-- Create a new string buffer being able
			-- to contain n characters.
		require
			non_negative_n: n >= 0
		ensure
			string_buffer_not_void: Result /= void;
			count_set: Result.count = n

	make_from_string (a_string: STRING): like string_buffer_type
			-- Create a new string buffer with characters from a_string.
		require
			a_string_not_void: a_string /= void
		ensure
			string_buffer_not_void: Result /= void;
			count_set: Result.count = a_string.count;
			charaters_set: equal (substring (Result, lower, a_string.count + lower - 1), a_string)
	
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

	string_buffer_: KL_STRING_BUFFER_ROUTINES
			-- Routines that ought to be in class STRING_BUFFER
			-- (from KL_IMPORTED_STRING_BUFFER_ROUTINES)
		ensure -- from KL_IMPORTED_STRING_BUFFER_ROUTINES
			string_buffer_routines_not_void: Result /= void

	substring (a_buffer: like string_buffer_type; s, e: INTEGER): STRING
			-- New string made up of characters held in
			-- a_buffer between indexes s and e
		require
			a_buffer_not_void: a_buffer /= void;
			s_large_enough: s >= lower;
			e_small_enough: e <= upper (a_buffer);
			valid_interval: s <= e + 1
		ensure
			substring_not_void: Result /= void;
			count_set: Result.count = e - s + 1
	
feature -- Measurement

	Lower: INTEGER is 0
			-- Lower index

	upper (a_buffer: like string_buffer_type): INTEGER
			-- Upper index
		require
			a_buffer_not_void: a_buffer /= void
		ensure
			definition: a_buffer.count = (Result - lower + 1)
	
feature -- Element change

	append_substring_to_string (a_buffer: like string_buffer_type; s, e: INTEGER; a_string: STRING)
			-- Append string made up of characters held in a_buffer
			-- between indexes s and e to a_string.
		require
			a_buffer_not_void: a_buffer /= void;
			a_string_not_void: a_string /= void;
			not_same: to_string_buffer (a_string) /= a_buffer;
			s_large_enough: s >= lower;
			e_small_enough: e <= upper (a_buffer);
			valid_interval: s <= e + 1
		ensure
			count_set: a_string.count = old (a_string.count) + (e - s + 1);
			charaters_set: s <= e implies equal (a_string.substring (old (a_string.count), a_string.count), substring (a_buffer, s, e))

	copy_from_stream (a_buffer: like string_buffer_type; pos: INTEGER; a_stream: like input_stream_type; 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_buffer_not_void: a_buffer /= void;
			pos_large_enough: pos >= lower;
			a_stream_not_void: a_stream /= void;
			a_stream_open_read: input_stream_.is_open_read (a_stream);
			nb_char_large_enough: nb_char >= 0;
			enough_space: (pos + nb_char - 1) <= upper (a_buffer)
		ensure
			nb_char_read_large_enough: Result >= 0;
			nb_char_read_small_enough: Result <= nb_char

	copy_from_string (a_buffer: like string_buffer_type; pos: INTEGER; a_string: STRING)
			-- Copy characters of a_string to a_buffer
			-- starting at position pos.
		require
			a_buffer_not_void: a_buffer /= void;
			a_string_not_void: a_string /= void;
			not_same: to_string_buffer (a_string) /= a_buffer;
			pos_large_enough: pos >= lower;
			enough_space: (pos + a_string.count - 1) <= upper (a_buffer)
		ensure
			charaters_set: equal (substring (a_buffer, pos, a_string.count + pos - 1), a_string)

	move_left (a_buffer: like string_buffer_type; old_pos, new_pos: INTEGER; nb: INTEGER)
			-- Copy nb characters from old_pos to
			-- new_pos in a_buffer.
		require
			a_buffer_not_void: a_buffer /= void;
			nb_positive: nb >= 0;
			old_pos_large_enough: old_pos >= lower;
			enough_characters: (old_pos + nb - 1) <= upper (a_buffer);
			new_pos_large_enough: new_pos >= lower;
			enough_space: (new_pos + nb - 1) <= upper (a_buffer);
			move_left: old_pos > new_pos

	move_right (a_buffer: like string_buffer_type; old_pos, new_pos: INTEGER; nb: INTEGER)
			-- Copy nb characters from old_pos to
			-- new_pos in a_buffer.
		require
			a_buffer_not_void: a_buffer /= void;
			nb_positive: nb >= 0;
			old_pos_large_enough: old_pos >= lower;
			enough_characters: (old_pos + nb - 1) <= upper (a_buffer);
			new_pos_large_enough: new_pos >= lower;
			enough_space: (new_pos + nb - 1) <= upper (a_buffer);
			move_right: old_pos < new_pos
	
feature -- Resizing

	resize (a_buffer: like string_buffer_type; n: INTEGER): like string_buffer_type
			-- Resize a_buffer so that it contains n characters.
			-- Do not lose any previously entered characters.
			-- Note: the returned string buffer might be a_buffer or
			-- a newly created string buffer where characters from
			-- a_buffer have been copied to.
		require
			a_buffer_not_void: a_buffer /= void;
			n_large_enough: n >= a_buffer.count
		ensure
			string_buffer_not_void: Result /= void;
			count_set: Result.count = n
	
feature -- Conversion

	to_string_buffer (a_string: STRING): like string_buffer_type
			-- String buffer filled with characters from a_string.
			-- The string buffer and a_string may share internal
			-- data. Use make_from_string if this is a concern.
		require
			a_string_not_void: a_string /= void
		ensure
			string_buffer_not_void: Result /= void;
			count_set: Result.count >= a_string.count;
			charaters_set: equal (substring (Result, lower, a_string.count + lower - 1), a_string)
	
feature -- Type anchors

	input_stream_type: IO_MEDIUM
			-- (from KL_IMPORTED_INPUT_STREAM_ROUTINES)

	string_buffer_type: SPECIAL [CHARACTER]
			-- (from KL_IMPORTED_STRING_BUFFER_ROUTINES)
	
invariant

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

end -- class KL_STRING_BUFFER_ROUTINES