indexing
	description: "Buffers storing command history entries"
	author: "Patrick Schoenbach"
	access: cursor
	contents: generic

deferred class interface
	HISTORY_CONTAINER [G -> COMMAND_HISTORY_ENTRY]

feature -- Access

	i_th (i: INTEGER): G
			-- i-th item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)

	index: INTEGER
			-- Current index
			-- (from SEQUENCIAL_CONTAINER)

	item: G
			-- Current item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
	
feature -- Measurement

	capacity: INTEGER
			-- Size of container
			-- (from SEQUENCIAL_CONTAINER)

	count: INTEGER
			-- Number of elements
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Status report

	after: BOOLEAN
			-- Is there no valid cursor position to the right of cursor?
			-- (from SEQUENCIAL_CONTAINER)

	before: BOOLEAN
			-- Is there no valid cursor position to the left of cursor?
			-- (from TWO_WAY_SEQUENCIAL_CONTAINER)

	empty: BOOLEAN
			-- Is container empty?
			-- (from SEQUENCIAL_CONTAINER)

	full: BOOLEAN
			-- Is container full?
			-- (from SEQUENCIAL_CONTAINER)

	insertable: BOOLEAN
			-- Can elements be inserted in the middle?
			-- (from SEQUENCIAL_CONTAINER)

	is_executed: BOOLEAN
			-- Has current item been executed?
			-- (from COMMAND_HISTORY)

	isfirst: BOOLEAN
			-- Is cursor on first element?
			-- (from SEQUENCIAL_CONTAINER)

	islast: BOOLEAN
			-- Is cursor on last element?
			-- (from SEQUENCIAL_CONTAINER)

	off: BOOLEAN
			-- Is there no current item?
			-- (from SEQUENCIAL_CONTAINER)

	prunable: BOOLEAN
			-- Is container prunable?
			-- (from SEQUENCIAL_CONTAINER)

	resizable: BOOLEAN
			-- Is container resizable?
			-- (from SEQUENCIAL_CONTAINER)

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Cursor movement

	back
			-- Move cursor backwards.
			-- (from TWO_WAY_SEQUENCIAL_CONTAINER)
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_before: not before

	finish
			-- Move cursor to last element.
			-- (from TWO_WAY_SEQUENCIAL_CONTAINER)
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from TWO_WAY_SEQUENCIAL_CONTAINER
			cursor_at_end: islast

	forth
			-- Move cursor forwards.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after

	go_i_th (i: INTEGER)
			-- Move cursor to the i-th position.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)
		ensure -- from SEQUENCIAL_CONTAINER
			i_th_position: index = i

	start
			-- Move cursor to first element.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from SEQUENCIAL_CONTAINER
			cursor_at_start: isfirst
	
feature -- Element change

	extend (v: G)
			-- Add v to the end of structure.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full

	put (v: G)
			-- Replace current item with v.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off

	put_left (v: G)
			-- Insert v to the right of cursor.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_before: not before

	put_right (v: G)
			-- Insert v to the right of cursor.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_after: not after
	
feature -- Removal

	remove
			-- Remove current item.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off

	wipe_out
			-- Empty container.
			-- (from SEQUENCIAL_CONTAINER)
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize container to n elements.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
feature -- Basic operations

	redo
			-- Redo command.
			-- (from COMMAND_HISTORY)

	undo
			-- Undo command.
			-- (from COMMAND_HISTORY)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	current_command_executed: not off implies item.is_executed;
		-- from TWO_WAY_SEQUENCIAL_CONTAINER
	off_definition: off = (before or after);
		-- from SEQUENCIAL_CONTAINER
	empty_definition: empty = (count = 0);
	off_definition: off = (before or after);
	empty_constraint: empty implies off;
	count_range: 0 <= count and count <= capacity;

end -- class HISTORY_CONTAINER