indexing
	description: "Objects that contains all the information relative to any header. Headers can only have email addresses informations."
	author: "David s"
	date: "$Date$"
	revision: "$Revision$"

class interface
	HEADER

create 

	make (item: STRING)
			-- Initialize the header with one 'item'.

	make_with_entries (list: ARRAY [STRING])
			-- Initialize the header with a 'list' of entries.

feature -- Initialization

	make (item: STRING)
			-- Initialize the header with one 'item'.

	make_with_entries (list: ARRAY [STRING])
			-- Initialize the header with a 'list' of entries.
	
feature -- Access

	entries: ARRAYED_LIST [STRING]
			-- Multiple entries.
	
feature -- Status report

	multiple_entries: BOOLEAN
			-- Has the header multiple entries.

	unique_entry: STRING
			-- Entry,
			-- Useful if not multiple entries.
		require
			has_unique_entry: not multiple_entries
	
feature -- Status setting

	enable_contains_addresses

	enable_multiple_entries
			-- Enable multiple entries.
	
feature -- Basic operations

	add_entries (list: ARRAY [STRING])
			-- Add multiple entries at once.
		require
			entries_exist: entries /= void

	add_entry (s: STRING)
			-- Add a new entry 's' to the header.
		ensure
			has_multiple_entries: multiple_entries
			entry_inserted: entries.has (s)

	remove_entry (entry: STRING)
			-- Remove 'entry'
		require
			has_entry: entries.has (entry)

	remove_i_th_entry (i: INTEGER)
			-- Remove 'i'-th entry.
		require
			valid_index: entries.valid_cursor_index (i)
	
invariant

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class HEADER