note

	status: "See notice at end of class.";
	date: "$Date$";
	revision: "$Revision$"

deferred class

	FONT_LIST_I

inherit
	G_ANY_I
		export
			{NONE} all
		undefine
			copy,
			is_equal
		end;

feature -- Access

	first: FONT
			-- Item at first position
		require
			not_empty: not empty
		deferred
		end;

	item: like first
			-- Item at cursor position
		require
			not_off: not off
		deferred
		end;

	i_th alias "[]" (i: INTEGER): like first
			-- Item at `i'_th position
		require
			index_large_enough: i >= 1;
			index_small_enough: i <= count;
		deferred
		end;

	last: like first
			-- Item at last position
		require
			not_empty: not empty
		deferred
		end;

	position: INTEGER
			-- Current cursor position, 0 if empty
		deferred
		end;

feature -- Measurement

	count: INTEGER
			-- Number of items in the chain
		deferred
		end

feature -- Status report

	empty: BOOLEAN
			-- Is the chain empty?
		deferred
		end;

	off: BOOLEAN
			-- Is cursor off?
		deferred
		end;

	offleft: BOOLEAN
			-- Is cursor off left edge?
		deferred
		end;

	offright: BOOLEAN
			-- Is cursor off right edge?
		deferred
		end;

	isfirst: BOOLEAN
			-- Is cursor at first position in the chain?
		deferred
		ensure
			Result implies (not empty)
		end;

	islast: BOOLEAN
			-- Is cursor at last position in the chain?
		deferred
		ensure
			Result implies (not empty)
		end;

feature -- Status setting

	destroy
			-- Destroy current font list.
		deferred
		end;

feature -- Cursor movement

	start
			-- Move cursor to first position.
		deferred
		ensure
			empty or isfirst
		end;

	finish
			-- Move cursor to last position
			-- (no effect if chain is empty).
		deferred
		ensure
			empty or islast
		end;

	forth
			-- Move cursor forward one position.
		require
			not empty and then position <= count
		deferred
		ensure
			position >= 1 and position <= count + 1
		end;

	back
			-- Move cursor backward one position.
		require
			not_offleft: position > 0
		deferred
		end;

	move (i: INTEGER)
			-- Move cursor `i' positions.
		require
			stay_right: position + i >= 0;
			stay_left: position + i <= count + 1;
			not_empty_unless_zero: empty implies i=0;
		deferred
		end;

	go (i: INTEGER)
			-- Move cursor to position `i'.
		require
			index_large_enough: i >= 0;
			index_small_enough: i <= count + 1;
			not_empty_unless_zero: empty implies i=0;
		deferred
		ensure
			position_set: position = i
		end;

	search_equal (v: like first)
			-- Move cursor to first position
			-- (at or after current cursor position)
			-- where item is equal to `v' (shallow equality);
			-- go off right if none.
		require
			search_element_exists: v /= Void
		deferred
		ensure
			valid: (not off) implies (v.is_equal (item))
		end;

	index_of (v: like first; i: INTEGER): INTEGER
			-- Index of `i'-th item `v'; 0 if none
		require
			positive_occurrence: i > 0
		deferred
		ensure
			positive_result: Result >= 0
		end;

	has (v: like first): BOOLEAN
			-- Does `v' appear in the chain ?
		deferred
		end

invariant
	empty_is_zero_cnt:
		empty = (count = 0);
	off_is_offleft_or_offright:
		off = ((position = 0) or else (position = count + 1));
	isfirst_is_pos_one:
		isfirst = (position = 1);
	islast_is_pos_cnt:
		islast = (not empty and (position = count));
	non_negative_count: count >= 0;
	non_negative_position: position >= 0
	stay_on: position <= count + 1;
	empty_implies_off: empty implies off;
	empty_implies_zero_pos:
		empty implies position = 0;
	not_on_empty:
		empty implies not (isfirst or islast)

note
	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
			 Eiffel Software
			 356 Storke Road, Goleta, CA 93117 USA
			 Telephone 805-685-1006, Fax 805-685-6869
			 Website http://www.eiffel.com
			 Customer support http://support.eiffel.com
		]"




end -- FONT_LIST_I