    indexing
    	description: "[Multi-column lists that allow in-place editing of list row items.  By default ALLcolumns are editable.  Only one single column item is editable at any time and the widget typewhich can be edited must conform to EV_TEXTABLE."
    	legal: "See notice at end of class."
    	status: "See notice at end of class."
    	date: "6/17/02"
    	revision: "1.0"

    class interface
    	EV_EDITABLE_LIST

    create
    	make (a_window: EV_WINDOW)
    			-- Create list with all columns editable and with relative 'a_window'.
    		require
    			window_not_void: a_window /= Void

    feature -- Initialization

    	make (a_window: EV_WINDOW)
    			-- Create list with all columns editable and with relative 'a_window'.
    		require
    			window_not_void: a_window /= Void

    feature -- Access

    	accept_cursor: EV_POINTER_STYLE
    			-- `Result' is cursor displayed when the screen pointer is over a
    			-- target that accepts pebble during pick and drop.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			result_not_void: Result /= Void
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.accept_cursor

    	actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_ABSTRACT_PICK_AND_DROPABLE]
    			-- Overrides default drop target on a certain position.
    			-- If `Void', `Current' will use the default drop target.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.actual_drop_target_agent

    	background_color: EV_COLOR
    			-- Color displayed behind foreground features.
    			-- (from EV_COLORIZABLE)
    		require -- from EV_COLORIZABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_COLORIZABLE
    			bridge_ok: Result.is_equal (implementation.background_color)

    	column_count: INTEGER_32
    			-- Column count.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.column_count

    	cursor: EV_DYNAMIC_LIST_CURSOR [EV_MULTI_COLUMN_LIST_ROW]
    			-- Current cursor position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from  CURSOR_STRUCTURE
    			True
    		ensure -- from CURSOR_STRUCTURE
    			cursor_not_void: Result /= Void
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result.is_equal (implementation.cursor)

    	data: ANY
    			-- Arbitrary user data may be stored here.
    			-- (from EV_ANY)

    	default_key_processing_handler: PREDICATE [ANY, TUPLE [EV_KEY]] assign set_default_key_processing_handler
    			-- Agent used to determine whether the default key processing should occur for Current.
    			-- If agent returns True then default key processing continues as normal, False prevents
    			-- default key processing from occurring.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.default_key_processing_handler

    	deny_cursor: EV_POINTER_STYLE
    			-- `Result' is cursor displayed when the screen pointer is over a
    			-- target that does not accept pebble during pick and drop.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			result_not_void: Result /= Void
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.deny_cursor

    	first: like item
    			-- Item at first position
    			-- (from CHAIN)
    		require -- from CHAIN
    			not_empty: not is_empty

    	foreground_color: EV_COLOR
    			-- Color of foreground features like text.
    			-- (from EV_COLORIZABLE)
    		require -- from EV_COLORIZABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_COLORIZABLE
    			bridge_ok: Result.is_equal (implementation.foreground_color)

    	generating_type: STRING_8
    			-- Name of current object's generating type
    			-- (type of which it is a direct instance)
    			-- (from ANY)

    	generator: STRING_8
    			-- Name of current object's generating class
    			-- (base class of the type of which it is a direct instance)
    			-- (from ANY)

    	has (v: like item): BOOLEAN
    			-- Does chain include `v'?
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from CHAIN)
    		require -- from  CONTAINER
    			True
    		ensure -- from CONTAINER
    			not_found_in_empty: Result implies not is_empty

    	help_context: FUNCTION [ANY, TUPLE, EV_HELP_CONTEXT]
    			-- Agent that evaluates to help context sent to help engine when help is requested
    			-- (from EV_HELP_CONTEXTABLE)
    		require -- from EV_HELP_CONTEXTABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_HELP_CONTEXTABLE
    			bridge_ok: Result = implementation.help_context

    	i_th alias "[]" (i: INTEGER_32): like item
    			-- Item at `i'-th position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from TABLE
    			valid_key: valid_index (i)
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result.is_equal (implementation.i_th (i))

    	frozen id_object (an_id: INTEGER_32): IDENTIFIED
    			-- Object associated with `an_id' (void if no such object)
    			-- (from IDENTIFIED)
    		ensure -- from IDENTIFIED
    			consistent: Result = Void or else Result.object_id = an_id

    	index: INTEGER_32
    			-- Current position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from  LINEAR
    			True
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result = implementation.index

    	index_of (v: like item; i: INTEGER_32): INTEGER_32
    			-- Index of `i'th occurrence of `v'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from LINEAR
    			positive_occurrences: i > 0
    		ensure -- from LINEAR
    			non_negative_result: Result >= 0
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result = implementation.index_of (v, i)

    	item: EV_MULTI_COLUMN_LIST_ROW
    			-- Item at current position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from TRAVERSABLE
    			not_off: not off
    		require -- from ACTIVE
    			readable: readable
    		ensure then -- from EV_DYNAMIC_LIST
    			not_void: Result /= Void
    			bridge_ok: Result.is_equal (implementation.item)

    	last: like item
    			-- Item at last position
    			-- (from CHAIN)
    		require -- from CHAIN
    			not_empty: not is_empty

    	frozen object_id: INTEGER_32
    			-- Unique for current object in any given session
    			-- (from IDENTIFIED)
    		ensure -- from IDENTIFIED
    			valid_id: id_object (Result) = Current

    	sequential_occurrences (v: like item): INTEGER_32
    			-- Number of times `v' appears.
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from LINEAR)
    		require -- from  BAG
    			True
    		ensure -- from BAG
    			non_negative_occurrences: Result >= 0

    	parent: EV_CONTAINER
    			-- Contains `Current'.
    			-- (from EV_WIDGET)
    		require -- from EV_CONTAINABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_WIDGET
    			bridge_ok: Result = implementation.parent

    	pebble: ANY
    			-- Data to be transported by pick and drop mechanism.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.pebble

    	pebble_function: FUNCTION [ANY, TUPLE, ANY]
    			-- Returns data to be transported by pick and drop mechanism.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.pebble_function

    	pebble_positioning_enabled: BOOLEAN
    			-- If `True' then pick and drop start coordinates are
    			-- pebble_x_position, pebble_y_position.
    			-- If `False' then pick and drop start coordinates are
    			-- the pointer coordinates.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.pebble_positioning_enabled

    	pebble_x_position: INTEGER_32
    			-- Initial x position for pick and drop relative to `Current'.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.pebble_x_position

    	pebble_y_position: INTEGER_32
    			-- Initial y position for pick and drop relative to `Current'.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.pebble_y_position

    	pixmaps_height: INTEGER_32
    			-- Height of displayed pixmaps in the list.
    			-- (from EV_ITEM_PIXMAP_SCALER)
    		require -- from EV_ITEM_PIXMAP_SCALER
    			not_destroyed: not is_destroyed
    		ensure -- from EV_ITEM_PIXMAP_SCALER
    			bridge_ok: Result = implementation.pixmaps_height

    	pixmaps_width: INTEGER_32
    			-- Width of displayed pixmaps in the list.
    			-- (from EV_ITEM_PIXMAP_SCALER)
    		require -- from EV_ITEM_PIXMAP_SCALER
    			not_destroyed: not is_destroyed
    		ensure -- from EV_ITEM_PIXMAP_SCALER
    			bridge_ok: Result = implementation.pixmaps_width

    	pointer_position: EV_COORDINATE
    			-- Position of the screen pointer relative to `Current'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			is_show_requested: is_show_requested

    	pointer_style: EV_POINTER_STYLE
    			-- Cursor displayed when pointer is over this widget.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    	real_target: EV_DOCKABLE_TARGET
    			-- `Result' is target used during a dockable transport if
    			-- mouse pointer is above `Current'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.real_target

    	retrieve_item_by_data (some_data: ANY; should_compare_objects: BOOLEAN): EV_MULTI_COLUMN_LIST_ROW
    			-- `Result' is first item in `Current' with data
    			-- matching `some_data'. Compare objects if
    			-- `should_compare_objects' otherwise compare references.
    			-- (from EV_DYNAMIC_LIST)
    		ensure -- from EV_DYNAMIC_LIST
    			not_found_in_empty: Result /= Void implies not is_empty
    			index_not_changed: old index = index

    	retrieve_items_by_data (some_data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_MULTI_COLUMN_LIST_ROW]
    			-- `Result' is all items in `Current' with data
    			-- matching `some_data'. Compare objects if
    			-- `should_compare_objects' otherwise compare references.
    			-- (from EV_DYNAMIC_LIST)
    		ensure -- from EV_DYNAMIC_LIST
    			result_not_void: Result /= Void
    			not_found_in_empty: not Result.is_empty implies not is_empty
    			index_not_changed: old index = index

    	row_height: INTEGER_32
    			-- Height in pixels of each row.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.row_height

    	selected_item: like item
    			-- Currently selected item.
    			-- Topmost selected item if multiple items are selected.
    			-- (For multiple selections see selected_items).
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.selected_item

    	selected_items: DYNAMIC_LIST [like item]
    			-- Currently selected items.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: lists_equal (Result, implementation.selected_items)

    	target_name: STRING_GENERAL
    			-- Optional textual name describing `Current' pick and drop hole.
    			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)

    	tooltip: STRING_32
    			-- Tooltip displayed on `Current'.
    			-- If `Result' is empty then no tooltip displayed.
    			-- (from EV_TOOLTIPABLE)
    		require -- from EV_TOOLTIPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_TOOLTIPABLE
    			bridge_ok: equal (Result, implementation.tooltip)
    			not_void: Result /= Void
    			cloned: Result /= implementation.tooltip

    	infix "@" (i: INTEGER_32): like item assign put_i_th
    			-- Item at `i'-th position
    			-- Was declared in CHAIN as synonym of i_th.
    			-- (from CHAIN)
    		require -- from TABLE
    			valid_key: valid_index (i)

    feature -- Measurement

    	count: INTEGER_32
    			-- Number of items.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from  FINITE
    			True
    		require -- from  SET
    			True
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result = implementation.count

    	index_set: INTEGER_INTERVAL
    			-- Range of acceptable indexes
    			-- (from CHAIN)
    		require -- from  INDEXABLE
    			True
    		ensure -- from INDEXABLE
    			not_void: Result /= Void
    		ensure then -- from CHAIN
    			count_definition: Result.count = count

    	occurrences (v: like item): INTEGER_32
    			-- Number of times `v' appears.
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from CHAIN)
    		require -- from  BAG
    			True
    		require -- from  LINEAR
    			True
    		ensure -- from BAG
    			non_negative_occurrences: Result >= 0

    	screen_x: INTEGER_32
    			-- Horizontal offset relative to left of screen in pixels.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.screen_x

    	screen_y: INTEGER_32
    			-- Vertical offset relative to top of screen in pixels.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.screen_y

    feature -- Comparison

    	frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void
    			-- or attached to isomorphic object structures?
    			-- (from ANY)
    		ensure -- from ANY
    			shallow_implies_deep: standard_equal (some, other) implies Result
    			both_or_none_void: (some = Void) implies (Result = (other = Void))
    			same_type: (Result and (some /= Void)) implies some.same_type (other)
    			symmetric: Result implies deep_equal (other, some)

    	frozen equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void or attached
    			-- to objects considered equal?
    			-- (from ANY)
    		ensure -- from ANY
    			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))

    	is_equal (other: like Current): BOOLEAN
    			-- Does `other' contain the same elements?
    			-- (from LIST)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			symmetric: Result implies other.is_equal (Current)
    			consistent: standard_is_equal (other) implies Result
    		ensure then -- from LIST
    			indices_unchanged: index = old index and other.index = old other.index
    			true_implies_same_size: Result implies count = other.count

    	frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void or attached to
    			-- field-by-field identical objects of the same type?
    			-- Always uses default object comparison criterion.
    			-- (from ANY)
    		ensure -- from ANY
    			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))

    	frozen standard_is_equal (other: like Current): BOOLEAN
    			-- Is `other' attached to an object of the same type
    			-- as current object, and field-by-field identical to it?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			same_type: Result implies same_type (other)
    			symmetric: Result implies other.standard_is_equal (Current)

    feature -- Status report

    	after: BOOLEAN
    			-- Is there no valid cursor position to the right of cursor?
    			-- (from LIST)
    		require -- from  LINEAR
    			True

    	all_columns_editable: BOOLEAN
    			-- Are all columns in the list editable?

    	all_rows_editable: BOOLEAN
    			-- Are all rows in the list editable?

    	before: BOOLEAN
    			-- Is there no valid cursor position to the left of cursor?
    			-- (from LIST)
    		require -- from  BILINEAR
    			True

    	column_alignment (a_column: INTEGER_32): EV_TEXT_ALIGNMENT
    			-- `Result' is alignment of column `a_column'.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column >= 1 and a_column <= column_count
    		ensure -- from EV_MULTI_COLUMN_LIST
    			result_not_void: Result /= Void
    			bridge_ok: Result.is_equal (implementation.column_alignment (a_column))

    	column_editable (i: INTEGER_32): BOOLEAN
    			-- Is column at index 'i' allowed to be edited?

    	column_title (a_column: INTEGER_32): STRING_32
    			-- Title of `a_column'.
    			-- Returns "" if no title given yet.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_positive: a_column >= 1
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result.is_equal (implementation.column_title (a_column))
    			cloned: Result /= implementation.column_title (a_column)

    	column_width (a_column: INTEGER_32): INTEGER_32
    			-- Width of `a_column' in pixels.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column >= 1 and a_column <= column_count
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.column_width (a_column)

    	conforms_to (other: ANY): BOOLEAN
    			-- Does type of current object conform to type
    			-- of `other' (as per Eiffel: The Language, chapter 13)?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void

    	exhausted: BOOLEAN
    			-- Has structure been completely explored?
    			-- (from LINEAR)
    		ensure -- from LINEAR
    			exhausted_when_off: off implies Result

    	extendible: BOOLEAN is True
    			-- May new items be added? (Answer: yes.)
    			-- (from DYNAMIC_CHAIN)

    	full: BOOLEAN is False
    			-- Is structured filled to capacity? (Answer: no.)
    			-- (from EV_DYNAMIC_LIST)

    	has_capture: BOOLEAN
    			-- Does widget have capture?
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.has_capture

    	has_focus: BOOLEAN
    			-- Does widget have the keyboard focus?
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.has_focus

    	is_displayed: BOOLEAN
    			-- Is `Current' visible on the screen?
    			-- `True' when show requested and parent displayed.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.is_displayed

    	is_dockable: BOOLEAN
    			-- Is `Current' dockable?
    			-- If `True', then `Current' may be dragged
    			-- from its current parent.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			bridge_ok: Result = implementation.is_dockable

    	is_empty: BOOLEAN
    			-- Is structure empty?
    			-- (from FINITE)
    		require -- from  CONTAINER
    			True

    	is_external_docking_enabled: BOOLEAN
    			-- Is `Current' able to be docked into an EV_DOCKABLE_DIALOG
    			-- When there is no valid EV_DRAGABLE_TARGET upon completion
    			-- of transport?
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			bridge_ok: Result = implementation.is_external_docking_enabled

    	is_external_docking_relative: BOOLEAN
    			-- Will dockable dialog displayed when `Current' is docked externally
    			-- be displayed relative to parent window of `Current'?
    			-- Otherwise displayed as a standard window.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			bridge_ok: Result = implementation.is_external_docking_relative

    	is_inserted (v: EV_MULTI_COLUMN_LIST_ROW): BOOLEAN
    			-- Has `v' been inserted by the most recent insertion?
    			-- (By default, the value returned is equivalent to calling
    			-- `has (v)'. However, descendants might be able to provide more
    			-- efficient implementations.)
    			-- (from COLLECTION)

    	is_sensitive: BOOLEAN
    			-- Is object sensitive to user input.
    			-- (from EV_SENSITIVE)
    		require -- from EV_SENSITIVE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_SENSITIVE
    			bridge_ok: Result = implementation.user_is_sensitive

    	is_show_requested: BOOLEAN
    			-- Will `Current' be displayed when its parent is?
    			-- See also is_displayed.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			bridge_ok: Result = implementation.is_show_requested

    	isfirst: BOOLEAN
    			-- Is cursor at first position?
    			-- (from CHAIN)
    		ensure -- from CHAIN
    			valid_position: Result implies not is_empty

    	islast: BOOLEAN
    			-- Is cursor at last position?
    			-- (from CHAIN)
    		ensure -- from CHAIN
    			valid_position: Result implies not is_empty

    	mode_is_drag_and_drop: BOOLEAN
    			-- Is the user interface mode drag and drop?
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.mode_is_drag_and_drop

    	mode_is_pick_and_drop: BOOLEAN
    			-- Is the user interface mode pick and drop?
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.mode_is_pick_and_drop

    	mode_is_target_menu: BOOLEAN
    			-- Is the user interface mode a pop-up menu of targets?
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_PICK_AND_DROPABLE
    			bridge_ok: Result = implementation.mode_is_target_menu

    	multiple_selection_enabled: BOOLEAN
    			-- Can more than one item be selected?
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.multiple_selection_enabled

    	object_comparison: BOOLEAN
    			-- Must search operations use equal rather than `='
    			-- for comparing references? (Default: no, use `='.)
    			-- (from CONTAINER)

    	off: BOOLEAN
    			-- Is there no current item?
    			-- (from CHAIN)
    		require -- from  TRAVERSABLE
    			True

    	prunable: BOOLEAN
    			-- May items be removed? (Answer: yes.)
    			-- (from DYNAMIC_CHAIN)
    		require -- from  COLLECTION
    			True

    	readable: BOOLEAN
    			-- Is there a current item that may be read?
    			-- (from SEQUENCE)
    		require -- from  ACTIVE
    			True

    	real_source: EV_DOCKABLE_SOURCE
    			-- `Result' is source to be dragged
    			--  when a docking drag occurs on `Current'.
    			-- If `Void', `Current' is dragged.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			bridge_ok: Result = implementation.real_source

    	row_editable (i: INTEGER_32): BOOLEAN
    			-- Is row at index 'i' allowed to be edited?

    	same_type (other: ANY): BOOLEAN
    			-- Is type of current object identical to type of `other'?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			definition: Result = (conforms_to (other) and other.conforms_to (Current))

    	set_pixmaps_size (a_width: INTEGER_32; a_height: INTEGER_32)
    			-- Set size of pixmaps disaplyed in `Current'.
    			-- Note: Default value is 16x16
    			-- (from EV_ITEM_PIXMAP_SCALER)
    		require -- from EV_ITEM_PIXMAP_SCALER
    			not_destroyed: not is_destroyed
    			valid_width: a_width > 0
    			valid_height: a_height > 0
    		ensure -- from EV_ITEM_PIXMAP_SCALER
    			width_set: pixmaps_width = a_width
    			height_set: pixmaps_height = a_height

    	title_shown: BOOLEAN
    			-- Is a row displaying column titles shown?
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			bridge_ok: Result = implementation.title_shown

    	valid_cursor (p: CURSOR): BOOLEAN
    			-- Can the cursor be moved to position `p'?
    			-- This is True if `p' conforms to EV_DYNAMIC_LIST_CURSOR and
    			-- if it points to an item, `Current' must have it.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from  CURSOR_STRUCTURE
    			True
    		ensure then -- from EV_DYNAMIC_LIST
    			bridge_ok: Result = implementation.valid_cursor (p)

    	valid_cursor_index (i: INTEGER_32): BOOLEAN
    			-- Is `i' correctly bounded for cursor movement?
    			-- (from CHAIN)
    		ensure -- from CHAIN
    			valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))

    	valid_index (i: INTEGER_32): BOOLEAN
    			-- Is `i' within allowable bounds?
    			-- (from CHAIN)
    		require -- from  TABLE
    			True
    		ensure then -- from INDEXABLE
    			only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
    		ensure then -- from CHAIN
    			valid_index_definition: Result = ((i >= 1) and (i <= count))

    	writable: BOOLEAN
    			-- Is there a current item that may be modified?
    			-- (from SEQUENCE)
    		require -- from  ACTIVE
    			True

    feature -- Status setting

    	align_text_center (a_column: INTEGER_32)
    			-- Display text of `a_column' centered.
    			-- First column is always left aligned.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 1 and a_column <= column_count
    		ensure -- from EV_MULTI_COLUMN_LIST
    			center_aligned: column_alignment (a_column).is_center_aligned

    	align_text_left (a_column: INTEGER_32)
    			-- Display text of `a_column' left aligned.
    			-- First column is always left aligned.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 1 and a_column <= column_count
    		ensure -- from EV_MULTI_COLUMN_LIST
    			left_aligned: column_alignment (a_column).is_left_aligned

    	align_text_right (a_column: INTEGER_32)
    			-- Display text of `a_column' right aligned.
    			-- First column is always left aligned.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 1 and a_column <= column_count
    		ensure -- from EV_MULTI_COLUMN_LIST
    			right_aligned: column_alignment (a_column).is_right_aligned

    	center_pointer
    			-- Position screen pointer over center of `Current'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    	compare_objects
    			-- Ensure that future search operations will use equal
    			-- rather than `=' for comparing references.
    			-- (from CONTAINER)
    		require -- from CONTAINER
    			changeable_comparison_criterion: changeable_comparison_criterion
    		ensure -- from CONTAINER
    			object_comparison

    	compare_references
    			-- Ensure that future search operations will use `='
    			-- rather than equal for comparing references.
    			-- (from CONTAINER)
    		require -- from CONTAINER
    			changeable_comparison_criterion: changeable_comparison_criterion
    		ensure -- from CONTAINER
    			reference_comparison: not object_comparison

    	disable_capture
    			-- Disable grab of all user input events.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			not_has_capture: not has_capture

    	disable_dockable
    			-- Ensure `Current' is not dockable.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			not_is_dockable: not is_dockable

    	disable_external_docking
    			-- Assign `False' to is_external_docking_enabled.
    			-- Forbid `Current' to be docked into an EV_DOCKABLE_DIALOG
    			-- When there is no valid EV_DRAGABLE_TARGET upon completion
    			-- of transport.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			is_dockable: is_dockable
    		ensure -- from EV_DOCKABLE_SOURCE
    			not_externally_dockable: not is_external_docking_enabled

    	disable_external_docking_relative
    			-- Assign `False' to is_external_docking_relative, ensuring that
    			-- a dockable dialog displayed when `Current' is docked externally
    			-- is displayed as a standard window.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			external_docking_enabled: is_external_docking_enabled
    		ensure -- from EV_DOCKABLE_SOURCE
    			external_docking_not_relative: not is_external_docking_relative

    	disable_multiple_selection
    			-- Allow only one item to be selected.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			not_multiple_selection_enabled: not multiple_selection_enabled

    	disable_pebble_positioning
    			-- Assign `False' to pebble_positioning_enabled.
    			-- The pick and drop will start at the pointer position.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			pebble_positioning_updated: not pebble_positioning_enabled

    	disable_sensitive
    			-- Make object non-sensitive to user input.
    			-- (from EV_SENSITIVE)
    		require -- from EV_SENSITIVE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_SENSITIVE
    			is_unsensitive: not is_sensitive

    	enable_capture
    			-- Grab all user input events (mouse and keyboard).
    			-- disable_capture must be called to resume normal input handling.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			is_displayed: is_displayed
    		ensure -- from EV_WIDGET
    			has_capture: has_capture

    	enable_dockable
    			-- Ensure `Current' is dockable.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			is_dockable: is_dockable

    	enable_external_docking
    			-- Assign `True' to is_external_docking_enabled.
    			-- Allows `Current' to be docked into an EV_DOCKABLE_DIALOG
    			-- When there is no valid EV_DRAGABLE_TARGET upon completion
    			-- of transport.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			is_dockable: is_dockable
    		ensure -- from EV_DOCKABLE_SOURCE
    			is_externally_dockable: is_external_docking_enabled

    	enable_external_docking_relative
    			-- Assign `True' to is_external_docking_relative, ensuring that
    			-- a dockable dialog displayed when `Current' is docked externally
    			-- is displayed relative to the top level window.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			external_docking_enabled: is_external_docking_enabled
    		ensure -- from EV_DOCKABLE_SOURCE
    			external_docking_not_relative: is_external_docking_relative

    	enable_multiple_selection
    			-- Allow more than one item to be selected.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			multiple_selection_enabled: multiple_selection_enabled

    	enable_pebble_positioning
    			-- Assign `True' to pebble_positioning_enabled.
    			-- Use pebble_x_position and pebble_y_position as the initial coordinates
    			-- for the pick and drop in pixels relative to `Current'.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			pebble_positioning_updated: pebble_positioning_enabled

    	enable_sensitive
    			-- Make object sensitive to user input.
    			-- (from EV_SENSITIVE)
    		require -- from EV_SENSITIVE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_SENSITIVE
    			is_sensitive: (parent = Void or parent_is_sensitive) implies is_sensitive

    	ensure_item_visible (an_item: EV_MULTI_COLUMN_LIST_ROW)
    			-- Ensure `an_item' is visible in `Current'.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			is_displayed: is_displayed
    			an_item_contained: has (an_item)

    	hide
    			-- Request that `Current' not be displayed even when its parent is.
    			-- If successful, make is_show_requested `False'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    	hide_title_row
    			-- Hide row displaying column titles.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			not_title_shown: not title_shown

    	remove_default_key_processing_handler
    			-- Ensure default_key_processing_handler is Void.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			default_key_processing_handler_removed: default_key_processing_handler = Void

    	remove_pebble
    			-- Make pebble `Void' and pebble_function `Void,
    			-- Removing transport.
    			-- (from EV_PICK_AND_DROPABLE)
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			pebble_removed: pebble = Void and pebble_function = Void

    	remove_real_source
    			-- Ensure real_source is `Void'.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_DOCKABLE_SOURCE
    			real_source_void: real_source = Void

    	remove_real_target
    			-- Ensure real_target is `Void'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    		ensure -- from EV_WIDGET
    			real_target_void: real_target = Void

    	remove_selection
    			-- Ensure that selected_items is empty.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			selected_items_empty: selected_items.is_empty

    	set_accept_cursor (a_cursor: like accept_cursor)
    			-- Set `a_cursor' to be displayed when the screen pointer is over a
    			-- target that accepts pebble during pick and drop.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			a_cursor_not_void: a_cursor /= Void
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			accept_cursor_assigned: accept_cursor.is_equal (a_cursor)

    	set_actual_drop_target_agent (an_agent: like actual_drop_target_agent)
    			-- Assign `an_agent' to actual_drop_target_agent.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			an_agent_not_void: an_agent /= Void
    		ensure -- from EV_WIDGET
    			assigned: actual_drop_target_agent = an_agent

    	set_default_colors
    			-- Set foreground and background color to their default values.
    			-- (from EV_COLORIZABLE)
    		require -- from EV_COLORIZABLE
    			not_destroyed: not is_destroyed

    	set_default_key_processing_handler (a_handler: like default_key_processing_handler)
    			-- Assign default_key_processing_handler to `a_handler'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    	set_deny_cursor (a_cursor: like deny_cursor)
    			-- Set `a_cursor' to be displayed when the screen pointer is not
    			-- over a valid target.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			a_cursor_not_void: a_cursor /= Void
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			deny_cursor_assigned: deny_cursor.is_equal (a_cursor)

    	set_drag_and_drop_mode
    			-- Set user interface mode to drag and drop.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			drag_and_drop_set: mode_is_drag_and_drop

    	set_focus
    			-- Grab keyboard focus.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			is_displayed: is_displayed
    			is_sensitive: is_sensitive

    	set_pebble (a_pebble: like pebble)
    			-- Assign `a_pebble' to pebble.
    			-- Overrides set_pebble_function.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			a_pebble_not_void: a_pebble /= Void
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			pebble_assigned: pebble = a_pebble

    	set_pebble_function (a_function: FUNCTION [ANY, TUPLE, ANY])
    			-- Set `a_function' to compute pebble.
    			-- It will be called once each time a pick occurs, the result
    			-- will be assigned to pebble for the duration of transport.
    			-- When a pick occurs, the pick position in widget coordinates,
    			-- <<x, y>> in pixels, is passed.
    			-- To handle this data use `a_function' of type
    			-- FUNCTION [ANY, TUPLE [INTEGER, INTEGER], ANY] and return the
    			-- pebble as a function of x and y.
    			-- Overrides set_pebble.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			a_function_not_void: a_function /= Void
    			a_function_takes_two_integer_open_operands: a_function.valid_operands ([1, 1])
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			pebble_function_assigned: pebble_function = a_function

    	set_pebble_position (a_x, a_y: INTEGER_32)
    			-- Set the initial position for pick and drop
    			-- Coordinates are in pixels and are relative to position of `Current'.
    			-- Pebble_positioning_enabled must be `True' for the position to be used,
    			-- use enable_pebble_positioning.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y

    	set_pick_and_drop_mode
    			-- Set user interface mode to pick and drop.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			pick_and_drop_set: mode_is_pick_and_drop

    	set_real_source (dockable_source: EV_DOCKABLE_SOURCE)
    			-- Assign `dockable_source' to real_source.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			is_dockable: is_dockable
    			dockable_source_not_void: dockable_source /= Void
    			dockable_source_is_parent_recursive: source_has_current_recursive (dockable_source)
    		ensure -- from EV_DOCKABLE_SOURCE
    			real_source_assigned: real_source = dockable_source

    	set_real_target (a_target: EV_DOCKABLE_TARGET)
    			-- Assign `a_target' to real_target.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			target_not_void: a_target /= Void
    		ensure -- from EV_WIDGET
    			assigned: real_target = a_target

    	set_target_menu_mode
    			-- Set user interface mode to pop-up menu of targets.
    			-- (from EV_PICK_AND_DROPABLE)
    		require -- from EV_PICK_AND_DROPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_PICK_AND_DROPABLE
    			target_menu_mode_set: mode_is_target_menu

    	set_target_name (a_name: STRING_GENERAL)
    			-- Assign `a_name' to target_name.
    			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
    		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			a_name_not_void: a_name /= Void
    		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
    			target_name_assigned: a_name /= target_name and a_name.is_equal (target_name)

    	show
    			-- Request that `Current' be displayed when its parent is.
    			-- `True' by default.
    			-- If successful, make is_show_requested `True'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    	show_title_row
    			-- Show row displaying column titles.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    		ensure -- from EV_MULTI_COLUMN_LIST
    			title_shown: title_shown

    feature -- Cursor movement

    	back
    			-- Move to previous position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from BILINEAR
    			not_before: not before

    	finish
    			-- Move cursor to last position.
    			-- (No effect if empty)
    			-- (from CHAIN)
    		require -- from  LINEAR
    			True
    		ensure then -- from CHAIN
    			at_last: not is_empty implies islast

    	forth
    			-- Move cursor to next position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from LINEAR
    			not_after: not after
    		ensure then -- from LIST
    			moved_forth: index = old index + 1

    	go_i_th (i: INTEGER_32)
    			-- Move cursor to `i'-th position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from CHAIN
    			valid_cursor_index: valid_cursor_index (i)
    		ensure -- from CHAIN
    			position_expected: index = i

    	go_to (p: CURSOR)
    			-- Move cursor to position `p'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from CURSOR_STRUCTURE
    			cursor_position_valid: valid_cursor (p)

    	move (i: INTEGER_32)
    			-- Move cursor `i' positions.
    			-- (from EV_DYNAMIC_LIST)
    		ensure -- from CHAIN
    			too_far_right: (old index + i > count) implies exhausted
    			too_far_left: (old index + i < 1) implies exhausted
    			expected_index: (not exhausted) implies (index = old index + i)

    	search (v: like item)
    			-- Move to first position (at or after current
    			-- position) where item and `v' are equal.
    			-- If structure does not include `v' ensure that
    			-- exhausted will be true.
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from BILINEAR)
    		ensure -- from LINEAR
    			object_found: (not exhausted and object_comparison) implies equal (v, item)
    			item_found: (not exhausted and not object_comparison) implies v = item

    	start
    			-- Move cursor to first position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from  TRAVERSABLE
    			True
    		ensure then -- from CHAIN
    			at_first: not is_empty implies isfirst
    		ensure then -- from EV_DYNAMIC_LIST
    			empty_implies_after: is_empty implies after

    feature -- Element change

    	append (s: SEQUENCE [like item])
    			-- Append a copy of `s'. Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			sequence_not_void: s /= Void
    			sequence_not_current: s /= Current
    			not_parented: not s.there_exists (agent (v: like item): BOOLEAN
    			)
    		ensure -- from EV_DYNAMIC_LIST
    			count_increased: old count + s.count = count
    			cursor_not_moved: (index = old index) or (after and old after)

    	fill (other: CONTAINER [EV_MULTI_COLUMN_LIST_ROW])
    			-- Fill with as many items of `other' as possible.
    			-- The representations of `other' and current structure
    			-- need not be the same.
    			-- (from CHAIN)
    		require -- from COLLECTION
    			other_not_void: other /= Void
    			extendible: extendible

    	force (v: like item)
    			-- Add `v' to end. Do not move cursor.
    			-- Was declared in EV_DYNAMIC_LIST as synonym of extend.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			v_is_last: v = last
    			count_increased: count = old count + 1
    			cursor_not_moved: (index = old index) or (after and old after)

    	dl_force (v: like item)
    			-- Add `v' to end.
    			-- (from SEQUENCE)
    		require -- from SEQUENCE
    			extendible: extendible
    		ensure then -- from SEQUENCE
    			new_count: count = old count + 1
    			item_inserted: has (v)

    	merge_left (other: like Current)
    			-- Merge `other' into current structure before cursor
    			-- position. Do not move cursor. Empty `other'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from DYNAMIC_CHAIN
    			extendible: extendible
    			not_before: not before
    			other_exists: other /= Void
    			not_current: other /= Current
    		ensure -- from DYNAMIC_CHAIN
    			new_count: count = old count + old other.count
    			new_index: index = old index + old other.count
    			other_is_empty: other.is_empty

    	merge_right (other: like Current)
    			-- Merge `other' into current structure after cursor
    			-- position. Do not move cursor. Empty `other'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from DYNAMIC_CHAIN
    			extendible: extendible
    			not_after: not after
    			other_exists: other /= Void
    			not_current: other /= Current
    		ensure -- from DYNAMIC_CHAIN
    			new_count: count = old count + old other.count
    			same_index: index = old index
    			other_is_empty: other.is_empty

    	put (v: like item)
    			-- Replace current item by `v'.
    			-- (Synonym for replace)
    			-- (from CHAIN)
    		require -- from COLLECTION
    			extendible: extendible
    		ensure -- from COLLECTION
    			item_inserted: is_inserted (v)
    		ensure then -- from SET
    			in_set_already: old has (v) implies (count = old count)
    			added_to_set: not old has (v) implies (count = old count + 1)
    		ensure then -- from CHAIN
    			same_count: count = old count

    	put_front (v: like item)
    			-- Add `v' at beginning. Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			v_is_first: v = first
    			count_increased: count = old count + 1
    			cursor_not_moved: (index = old index + 1) or (before and old before)

    	put_i_th (v: like item; i: INTEGER_32)
    			-- Replace item at `i'-th position by `v'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			valid_index: i > 0 and i <= count
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			item_replaced: v = i_th (i)
    			not_has_old_item: not has (old i_th (i))
    			old_item_parent_void: (old i_th (i)).parent = Void
    			count_same: count = old count
    			cursor_not_moved: index = old index

    	put_left (v: like item)
    			-- Add `v' to the left of cursor position. Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			not_before: not before
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			v_at_index_plus_one: v = i_th (index - 1)
    			count_increased: count = old count + 1
    			cursor_not_moved: index = old index + 1

    	put_right (v: like item)
    			-- Add `v' to right of cursor position. Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			not_after: not after
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			v_at_index_plus_one: v = i_th (index + 1)
    			count_increased: count = old count + 1
    			cursor_not_moved: index = old index

    	remove_help_context
    			-- Remove key press action associated with `EV_APPLICATION.help_key'.
    			-- (from EV_HELP_CONTEXTABLE)
    		require -- from EV_HELP_CONTEXTABLE
    			not_destroyed: not is_destroyed
    			help_context_not_void: help_context /= Void
    		ensure -- from EV_HELP_CONTEXTABLE
    			no_help_context: help_context = Void

    	remove_tooltip
    			-- Make tooltip empty.
    			-- (from EV_TOOLTIPABLE)
    		require -- from EV_TOOLTIPABLE
    			not_destroyed: not is_destroyed
    		ensure -- from EV_TOOLTIPABLE
    			tooltip_removed: tooltip.is_empty

    	replace (v: like item)
    			-- Replace current item by `v'.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			writable: writable
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			item_replaced: v = item
    			not_has_old_item: not has (old item)
    			old_item_parent_void: (old item).parent = Void
    			count_same: count = old count
    			cursor_not_moved: index = old index

    	resize_column_to_content (a_column: INTEGER_32)
    			-- Resize column `a_column' to width of its widest text.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 0 and a_column <= column_count

    	set_background_color (a_color: like background_color)
    			-- Assign `a_color' to background_color.
    			-- (from EV_COLORIZABLE)
    		require -- from EV_COLORIZABLE
    			not_destroyed: not is_destroyed
    			a_color_not_void: a_color /= Void
    		ensure -- from EV_COLORIZABLE
    			background_color_assigned: background_color.is_equal (a_color)

    	set_column_alignment (an_alignment: EV_TEXT_ALIGNMENT; a_column: INTEGER_32)
    			-- Align the text of column `a_column' to `an_alignment'
    			-- The first column must stay as left aligned as MSDN
    			-- states that the first column can only be set as left aligned
    			-- for Win32.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 1 and a_column <= column_count
    			alignment_not_void: an_alignment /= Void
    		ensure -- from EV_MULTI_COLUMN_LIST
    			column_alignment_assigned: column_alignment (a_column).is_equal (an_alignment)

    	set_column_alignments (alignments: LINKED_LIST [EV_TEXT_ALIGNMENT])
    			-- Assign `alignments' to column text alignments in order.
    			-- The first alignment element is ignored
    			-- (see set_column_alignment).
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			alignments_not_void: alignments /= Void
    		ensure -- from EV_MULTI_COLUMN_LIST
    			column_alignments_assigned: column_alignments_assigned (alignments)

    	set_column_title (a_title: STRING_GENERAL; a_column: INTEGER_32)
    			-- Assign `a_title' to the column_title(`a_column').
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_positive: a_column > 0
    			a_title_not_void: a_title /= Void
    		ensure -- from EV_MULTI_COLUMN_LIST
    			a_title_assigned: column_title (a_column).is_equal (a_title)
    			column_count_valid: column_count >= a_column
    			cloned: column_title (a_column) /= a_title

    	set_column_titles (titles: ARRAY [STRING_GENERAL])
    			-- Assign `titles' to titles of columns in order.
    			-- `Current' will resize if the number of titles exceeds
    			-- column_count.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			titles_not_void: titles /= Void
    		ensure -- from EV_MULTI_COLUMN_LIST
    			column_count_valid: column_count >= titles.count
    			column_titles_assigned: column_titles_assigned (titles)

    	set_column_width (a_width: INTEGER_32; a_column: INTEGER_32)
    			-- Assign `a_width' column_width(`a_column').
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			a_column_within_range: a_column > 0
    			a_width_positive: a_width >= 0
    		ensure -- from EV_MULTI_COLUMN_LIST
    			column_count_valid: column_count >= a_column
    			a_width_assigned: a_width = column_width (a_column)

    	set_column_widths (widths: ARRAY [INTEGER_32])
    			-- Assign `widths' to column widths in order.
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_MULTI_COLUMN_LIST
    			not_destroyed: not is_destroyed
    			widths_not_void: widths /= Void
    		ensure -- from EV_MULTI_COLUMN_LIST
    			column_count_valid: column_count >= widths.count
    			column_widths_assigned: column_widths_assigned (widths)

    	set_data (some_data: like data)
    			-- Assign `some_data' to data.
    			-- (from EV_ANY)
    		require -- from EV_ANY
    			not_destroyed: not is_destroyed
    		ensure -- from EV_ANY
    			data_assigned: data = some_data

    	set_foreground_color (a_color: like foreground_color)
    			-- Assign `a_color' to foreground_color.
    			-- (from EV_COLORIZABLE)
    		require -- from EV_COLORIZABLE
    			not_destroyed: not is_destroyed
    			a_color_not_void: a_color /= Void
    		ensure -- from EV_COLORIZABLE
    			foreground_color_assigned: foreground_color.is_equal (a_color)

    	set_help_context (an_help_context: like help_context)
    			-- Assign `an_help_context' to help_context.
    			-- (from EV_HELP_CONTEXTABLE)
    		require -- from EV_HELP_CONTEXTABLE
    			not_destroyed: not is_destroyed
    			an_help_context_not_void: an_help_context /= Void
    		ensure -- from EV_HELP_CONTEXTABLE
    			help_context_assigned: help_context.is_equal (an_help_context)

    	set_minimum_height (a_minimum_height: INTEGER_32)
    			-- Set `a_minimum_height' in pixels to minimum_height.
    			-- If height is less than `a_minimum_height', resize.
    			-- From now, minimum_height is fixed and will not be changed
    			-- dynamically by the application anymore.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			a_minimum_height_positive: a_minimum_height >= 0
    		ensure -- from EV_WIDGET
    			minimum_height_assigned: minimum_height = a_minimum_height
    			minimum_height_set_by_user_set: minimum_height_set_by_user

    	set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32)
    			-- Assign `a_minimum_height' to minimum_height
    			-- and `a_minimum_width' to minimum_width in pixels.
    			-- If width or height is less than minimum size, resize.
    			-- From now, minimum size is fixed and will not be changed
    			-- dynamically by the application anymore.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			a_minimum_width_positive: a_minimum_width >= 0
    			a_minimum_height_positive: a_minimum_height >= 0
    		ensure -- from EV_WIDGET
    			minimum_width_assigned: minimum_width = a_minimum_width
    			minimum_height_assigned: minimum_height = a_minimum_height
    			minimum_height_set_by_user_set: minimum_height_set_by_user
    			minimum_width_set_by_user_set: minimum_width_set_by_user

    	set_minimum_width (a_minimum_width: INTEGER_32)
    			-- Assign `a_minimum_width' in pixels to minimum_width.
    			-- If width is less than `a_minimum_width', resize.
    			-- From now, minimum_width is fixed and will not be changed
    			-- dynamically by the application anymore.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			a_minimum_width_positive: a_minimum_width >= 0
    		ensure -- from EV_WIDGET
    			minimum_width_assigned: minimum_width = a_minimum_width
    			minimum_width_set_by_user_set: minimum_width_set_by_user

    	set_pointer_style (a_cursor: like pointer_style)
    			-- Assign `a_cursor' to pointer_style.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed
    			a_cursor_not_void: a_cursor /= Void
    		ensure -- from EV_WIDGET
    			pointer_style_assigned: pointer_style.is_equal (a_cursor)

    	set_tooltip (a_tooltip: STRING_GENERAL)
    			-- Assign `a_tooltip' to tooltip.
    			-- (from EV_TOOLTIPABLE)
    		require -- from EV_TOOLTIPABLE
    			not_destroyed: not is_destroyed
    			tooltip: a_tooltip /= Void
    		ensure -- from EV_TOOLTIPABLE
    			tooltip_assigned: tooltip.is_equal (a_tooltip)
    			cloned: tooltip /= a_tooltip

    	swap (i: INTEGER_32)
    			-- Exchange_item at `i'-th position with item
    			-- at cursor position.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from CHAIN
    			not_off: not off
    			valid_index: valid_index (i)
    		ensure -- from CHAIN
    			swapped_to_item: item = old i_th (i)
    			swapped_from_item: i_th (i) = old item

    feature -- Removal

    	prune (v: like item)
    			-- Remove `v' if present. Do not move cursor, except if
    			-- cursor was on `v', move to right neighbor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure then -- from SET
    			removed_count_change: old has (v) implies (count = old count - 1)
    			not_removed_no_count_change: not old has (v) implies (count = old count)
    			item_deleted: not has (v)
    		ensure then -- from EV_DYNAMIC_LIST
    			not_has_v: not has (v)
    			had_item_implies_parent_void: old has (v) implies v.parent = Void
    			had_item_implies_count_decreased: old has (v) implies count = old count - 1
    			had_item_and_was_after_implies_index_decreased: (old after and old has (v)) implies index = old index - 1

    	prune_all (v: like item)
    			-- Remove all occurrences of `v'.
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- Leave structure exhausted.
    			-- (from DYNAMIC_CHAIN)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure -- from COLLECTION
    			no_more_occurrences: not has (v)
    		ensure then -- from DYNAMIC_CHAIN
    			is_exhausted: exhausted

    	remove
    			-- Remove current item. Move cursor to right neighbor.
    			-- (or after if no right neighbor).
    			-- (from EV_DYNAMIC_LIST)
    		require -- from ACTIVE
    			prunable: prunable
    			writable: writable
    		ensure then -- from DYNAMIC_LIST
    			after_when_empty: is_empty implies after
    		ensure then -- from EV_DYNAMIC_LIST
    			v_removed: not has (old item)
    			parent_void: (old item).parent = Void
    			count_decreased: count = old count - 1
    			index_same: index = old index

    	remove_left
    			-- Remove item to left of cursor position.
    			-- Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from DYNAMIC_CHAIN
    			left_exists: index > 1
    		ensure -- from DYNAMIC_CHAIN
    			new_count: count = old count - 1
    			new_index: index = old index - 1
    		ensure then -- from EV_DYNAMIC_LIST
    			left_neighbor_removed: not has (old i_th (index - 1))
    			parent_void: (old i_th (index - 1)).parent = Void
    			index_decreased: index = old index - 1

    	remove_right
    			-- Remove item to right of cursor position.
    			-- Do not move cursor.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from DYNAMIC_CHAIN
    			right_exists: index < count
    		ensure -- from DYNAMIC_CHAIN
    			new_count: count = old count - 1
    			same_index: index = old index
    		ensure then -- from EV_DYNAMIC_LIST
    			right_neighbor_removed: not has (old i_th (index + 1))
    			parent_void: (old i_th (index + 1)).parent = Void
    			index_same: index = old index

    	remove_selected_item
    			-- Remove the currently selected item from the list.

    	wipe_out
    			-- Remove all items.
    			-- (from EV_DYNAMIC_LIST)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure -- from COLLECTION
    			wiped_out: is_empty
    		ensure then -- from DYNAMIC_LIST
    			is_before: before

    feature -- Conversion

    	linear_representation: LINEAR [EV_MULTI_COLUMN_LIST_ROW]
    			-- Representation as a linear structure
    			-- (from LINEAR)
    		require -- from  CONTAINER
    			True

    feature -- Duplication

    	copy (other: like Current)
    			-- Update current object using fields of object attached
    			-- to `other', so as to yield equal objects.
    			-- (from EV_ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    			type_identity: same_type (other)
    		ensure -- from ANY
    			is_equal: is_equal (other)

    	frozen deep_copy (other: like Current)
    			-- Effect equivalent to that of:
    			--		copy (`other' . deep_twin)
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			deep_equal: deep_equal (Current, other)

    	frozen deep_twin: like Current
    			-- New object structure recursively duplicated from Current.
    			-- (from ANY)
    		ensure -- from ANY
    			deep_equal: deep_equal (Current, Result)

    	frozen standard_copy (other: like Current)
    			-- Copy every field of `other' onto corresponding field
    			-- of current object.
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    			type_identity: same_type (other)
    		ensure -- from ANY
    			is_standard_equal: standard_is_equal (other)

    	frozen standard_twin: like Current
    			-- New object field-by-field identical to `other'.
    			-- Always uses default copying semantics.
    			-- (from ANY)
    		ensure -- from ANY
    			standard_twin_not_void: Result /= Void
    			equal: standard_equal (Result, Current)

    	frozen twin: like Current
    			-- New object equal to `Current'
    			-- twin calls copy; to change copying/twining semantics, redefine copy.
    			-- (from ANY)
    		ensure -- from ANY
    			twin_not_void: Result /= Void
    			is_equal: Result.is_equal (Current)

    feature -- Basic operations

    	frozen default: like Current
    			-- Default value of object's type
    			-- (from ANY)

    	frozen default_pointer: POINTER
    			-- Default value of type `POINTER'
    			-- (Avoid the need to write `p'.default for
    			-- some `p' of type `POINTER'.)
    			-- (from ANY)

    	default_rescue
    			-- Process exception for routines with no Rescue clause.
    			-- (Default: do nothing.)
    			-- (from ANY)

    	frozen do_nothing
    			-- Execute a null action.
    			-- (from ANY)

    	refresh_now
    			-- Force an immediate redraw of `Current'.
    			-- (from EV_WIDGET)
    		require -- from EV_WIDGET
    			not_destroyed: not is_destroyed

    feature -- Implementation

    	changeable_comparison_criterion: BOOLEAN is False
    			-- May object_comparison be changed?
    			-- (Answer: no by default.
    			-- (from EV_ITEM_LIST)

    feature -- Actions

    	end_edit_actions: ACTION_SEQUENCE [TUPLE]
    			-- List of actions to perform when list row has just been edited.

    feature -- Command

    	destroy
    			-- Destroy underlying native toolkit object.
    			-- Render `Current' unusable.
    			-- (from EV_ANY)
    		ensure -- from EV_ANY
    			is_destroyed: is_destroyed

    feature -- Contract support

    	is_parent_recursive (a_row: EV_MULTI_COLUMN_LIST_ROW): BOOLEAN
    			-- Is `a_row' a parent of `Current'?
    			-- (from EV_MULTI_COLUMN_LIST)
    		require -- from EV_DYNAMIC_LIST
    			a_list_not_void: a_row /= Void
    			not_destroyed: not is_destroyed

    	parent_of_source_allows_docking: BOOLEAN
    			-- Does parent of source to be transported
    			-- allow current to be dragged out? (See real_source)
    			-- Not all Vision2 containers are currently supported by this
    			-- mechanism, only descendents of EV_DOCKABLE_TARGET
    			-- are supported.
    			-- (from EV_DOCKABLE_SOURCE)

    	same (other: EV_ANY): BOOLEAN
    			-- Is `other' `Current'?
    			-- (from EV_DYNAMIC_LIST)

    	source_has_current_recursive (source: EV_DOCKABLE_SOURCE): BOOLEAN
    			-- Does `source' recursively contain `Current'?
    			-- As seen by parenting structure.
    			-- (from EV_DOCKABLE_SOURCE)
    		require -- from EV_DOCKABLE_SOURCE
    			not_destroyed: not is_destroyed
    			source_not_void: source /= Void

    feature -- Editing

    	edit_row (x, y, button: INTEGER_32; x_tilt, y_tilt, pressure: REAL_64; a_screen_x, a_screen_y: INTEGER_32)
    			-- User has double clicked list row so set up dialogs for in-place editing.

    feature -- Element Change

    	extend (v: like item)
    			-- Add 'v' to Current.
    		require -- from EV_DYNAMIC_LIST
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			v_not_void: v /= Void
    			v_parent_void: v.parent = Void
    			v_not_current: not same (v)
    			v_not_parent_of_current: not is_parent_recursive (v)
    		ensure -- from EV_DYNAMIC_LIST
    			parent_is_current: v.parent = Current
    			v_is_last: v = last
    			count_increased: count = old count + 1
    			cursor_not_moved: (index = old index) or (after and old after)

    feature -- Event handling

    	column_resized_actions: EV_COLUMN_ACTION_SEQUENCE
    			-- Actions to be performed when a column has been resized.
    			-- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES)
    		ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
    			not_void: Result /= Void

    	column_title_click_actions: EV_COLUMN_ACTION_SEQUENCE
    			-- Actions to be performed when a column title is clicked.
    			-- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES)
    		ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
    			not_void: Result /= Void

    	conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when a pebble that fits here is picked.
    			-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	deselect_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE
    			-- Actions to be performed when a row is deselected.
    			-- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES)
    		ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
    			not_void: Result /= Void

    	dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed after a dock completes from `Current'.
    			-- Either to a dockable target or a dockable dialog.
    			-- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES)
    		ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when a dockable source is dragged.
    			-- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES)
    		ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	drop_actions: EV_PND_ACTION_SEQUENCE
    			-- Actions to be performed when a pebble is dropped here.
    			-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when keyboard focus is gained.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when keyboard focus is lost.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	key_press_actions: EV_KEY_ACTION_SEQUENCE
    			-- Actions to be performed when a keyboard key is pressed.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE
    			-- Actions to be performed when a keyboard press generates a displayable character.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	key_release_actions: EV_KEY_ACTION_SEQUENCE
    			-- Actions to be performed when a keyboard key is released.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE
    			-- Actions to be performed when mouse wheel is rotated.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pick_actions: EV_PND_START_ACTION_SEQUENCE
    			-- Actions to be performed when pebble is picked up.
    			-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE
    			-- Actions to be performed when a transport from `Current' ends.
    			-- If transport completed successfully, then event data
    			-- is target. If cancelled, then event data is Void.
    			-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
    		ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer button is pressed.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer button is released.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer is double clicked.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer enters widget.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer leaves widget.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE
    			-- Actions to be performed when screen pointer moves.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
    			True
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
    			-- Actions to be performed when size changes.
    			-- (from EV_WIDGET_ACTION_SEQUENCES)
    		ensure -- from EV_WIDGET_ACTION_SEQUENCES
    			not_void: Result /= Void

    	select_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE
    			-- Actions to be performed when a row is selected.
    			-- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES)
    		ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
    			not_void: Result /= Void

    feature -- Iteration

    	do_all (action: PROCEDURE [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW]])
    			-- Apply `action' to every item.
    			-- Semantics not guaranteed if `action' changes the structure;
    			-- in such a case, apply iterator to clone of structure instead.
    			-- (from LINEAR)
    		require -- from TRAVERSABLE
    			action_exists: action /= Void

    	do_if (action: PROCEDURE [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW]]; test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN])
    			-- Apply `action' to every item that satisfies `test'.
    			-- Semantics not guaranteed if `action' or `test' changes the structure;
    			-- in such a case, apply iterator to clone of structure instead.
    			-- (from LINEAR)
    		require -- from TRAVERSABLE
    			action_exists: action /= Void
    			test_exits: test /= Void

    	for_all (test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN]): BOOLEAN
    			-- Is `test' true for all items?
    			-- Semantics not guaranteed if `test' changes the structure;
    			-- in such a case, apply iterator to clone of structure instead.
    			-- (from LINEAR)
    		require -- from TRAVERSABLE
    			test_exits: test /= Void
    		ensure then -- from LINEAR
    			empty: is_empty implies Result

    	there_exists (test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN]): BOOLEAN
    			-- Is `test' true for at least one item?
    			-- Semantics not guaranteed if `test' changes the structure;
    			-- in such a case, apply iterator to clone of structure instead.
    			-- (from LINEAR)
    		require -- from TRAVERSABLE
    			test_exits: test /= Void

    feature -- Measurement

    	height: INTEGER_32
    			-- Vertical size in pixels.
    			-- Same as minimum_height when not displayed.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.height

    	minimum_height: INTEGER_32
    			-- Lower bound on height in pixels.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.minimum_height
    			positive_or_zero: Result >= 0

    	minimum_width: INTEGER_32
    			-- Lower bound on width in pixels.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.minimum_width
    			positive_or_zero: Result >= 0

    	width: INTEGER_32
    			-- Horizontal size in pixels.
    			-- Same as minimum_width when not displayed.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.width

    	x_position: INTEGER_32
    			-- Horizontal offset relative to parent x_position in pixels.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.x_position

    	y_position: INTEGER_32
    			-- Vertical offset relative to parent y_position in pixels.
    			-- (from EV_POSITIONED)
    		require -- from EV_POSITIONED
    			not_destroyed: not is_destroyed
    		ensure -- from EV_POSITIONED
    			bridge_ok: Result = implementation.y_position

    feature -- Output

    	io: STD_FILES
    			-- Handle to standard file setup
    			-- (from ANY)

    	out: STRING_8
    			-- New string containing terse printable representation
    			-- of current object
    			-- Was declared in ANY as synonym of tagged_out.
    			-- (from ANY)

    	print (some: ANY)
    			-- Write terse external representation of `some'
    			-- on standard output.
    			-- (from ANY)

    	frozen tagged_out: STRING_8
    			-- New string containing terse printable representation
    			-- of current object
    			-- Was declared in ANY as synonym of out.
    			-- (from ANY)

    feature -- Platform

    	operating_environment: OPERATING_ENVIRONMENT
    			-- Objects available from the operating system
    			-- (from ANY)

    feature -- Selection

    	select_item (a_string: STRING_GENERAL; i: INTEGER_32)
    			-- Select in list the first item with text 'a_string' at index 'i'.

    feature -- Status Report

    	is_destroyed: BOOLEAN
    			-- Is `Current' no longer usable?
    			-- (from EV_ANY)
    		ensure -- from EV_ANY
    			bridge_ok: Result = implementation.is_destroyed

    feature -- Status setting

    	change_widget_type (i: INTEGER_32; a_widget: EV_TEXTABLE)
    			-- Set widget type to be displayed at column index 'i'
    		require
    			editable_column: column_editable (i)

    	set_all_columns_editable
    			-- Make every column editable.
    		require
    			has_columns: column_count > 0

    	set_all_rows_editable
    			-- Make every row editable.

    	set_column_editable (a_flag: BOOLEAN; i: INTEGER_32)
    			-- Make column at index 'i' editable according to 'a_flag'.

    	set_non_empty_column_values (a_flag: BOOLEAN)
    			-- Set so edited column values are not allowed to be empty.

    	set_row_editable (a_flag: BOOLEAN; i: INTEGER_32)
    			-- Make row at index 'i' editable according to 'a_flag'.

    	set_unique_column_values (a_flag: BOOLEAN)
    			-- Set column value uniqueness to 'a_flag'.

    	set_with_previous_text
    			-- Set field at row index 'widget_row' and column index 'widget_column' with
    			-- value of `saved text' after an edit has been unsuccessful

    invariant
    	has_relative_window: relative_window /= Void
    	change_widgets_not_void: change_widgets /= Void
    	editable_columns_not_void: editable_columns /= Void

    		-- from EV_WIDGET
    	pointer_position_not_void: is_usable and is_show_requested implies pointer_position /= Void
    	is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested
    	parent_contains_current: is_usable and then parent /= Void implies parent.has (Current)

    		-- from EV_PICK_AND_DROPABLE
    	user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1

    		-- from EV_ANY
    	is_initialized: is_initialized
    	is_coupled: implementation /= Void and then implementation.interface = Current
    	default_create_called: default_create_called

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

    		-- from EV_DOCKABLE_SOURCE
    	parent_permits_docking: is_dockable implies parent_of_source_allows_docking

    		-- from EV_COLORIZABLE
    	background_color_not_void: is_usable implies background_color /= Void
    	foreground_color_not_void: is_usable implies foreground_color /= Void

    		-- from EV_POSITIONED
    	width_not_negative: is_usable implies width >= 0
    	height_not_negative: is_usable implies height >= 0
    	minimum_width_not_negative: is_usable implies minimum_width >= 0
    	minimum_height_not_negative: is_usable implies minimum_height >= 0

    		-- from EV_ITEM_LIST
    	parent_of_items_is_current: is_usable and then not is_empty implies parent_of_items_is_current
    	items_unique: is_usable and not is_empty implies items_unique

    		-- from LIST
    	before_definition: before = (index = 0)
    	after_definition: after = (index = count + 1)

    		-- from CHAIN
    	non_negative_index: index >= 0
    	index_small_enough: index <= count + 1
    	off_definition: off = ((index = 0) or (index = count + 1))
    	isfirst_definition: isfirst = ((not is_empty) and (index = 1))
    	islast_definition: islast = ((not is_empty) and (index = count))
    	item_corresponds_to_index: (not off) implies (item = i_th (index))
    	index_set_has_same_count: index_set.count = count

    		-- from ACTIVE
    	writable_constraint: writable implies readable
    	empty_constraint: is_empty implies (not readable) and (not writable)

    		-- from INDEXABLE
    	index_set_not_void: index_set /= Void

    		-- from BILINEAR
    	not_both: not (after and before)
    	before_constraint: before implies off

    		-- from LINEAR
    	after_constraint: after implies off

    		-- from TRAVERSABLE
    	empty_constraint: is_empty implies off

    		-- from FINITE
    	empty_definition: is_empty = (count = 0)
    	non_negative_count: count >= 0

    		-- from DYNAMIC_CHAIN
    	extendible: extendible

    		-- from EV_ITEM_PIXMAP_SCALER
    	pixmaps_size_positive: pixmaps_height > 0 and pixmaps_width > 0

    indexing
    	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 -- class EV_EDITABLE_LIST