Automatic generation produced by ISE Eiffel

Classes
Clusters
Cluster hierarchy
Chart
Relations
Flat contracts
Go to: 
note
	description: "Horizontal box for display elements"
	legal: "See notice at end of class."
	status: "See notice at end of class."
	date: "$Date: 2008-12-29 11:27:11 -0900 (Mon, 29 Dec 2008) $"
	revision: "$Revision: 76420 $"

class interface
	DV_HORIZONTAL_BOX

create 
	make
			-- Initialize.
			-- (from DV_BOX)

	make_without_borders
			-- Initialize.
			-- Box has no borders: use this to have a nice display
			-- when box is contained in another box. 
			-- (from DV_BOX)

feature -- Initialization

	make
			-- Initialize.
			-- (from DV_BOX)

	make_without_borders
			-- Initialize.
			-- Box has no borders: use this to have a nice display
			-- when box is contained in another box. 
			-- (from DV_BOX)

	set_default
			-- Initialize default values
			-- (from DV_BOX)
	
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
			cursor_valid: (attached implementation.accept_cursor implies Result = implementation.accept_cursor) or else Result = Default_pixmaps.Standard_cursor

	actual_drop_target_agent: detachable FUNCTION [INTEGER_32, INTEGER_32, detachable 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

	at alias "@" (i: INTEGER_32): like item assign dl_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)

	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)

	background_pixmap: detachable EV_PIXMAP
			-- Result is pixmap displayed on background of Current.
			-- It is tessellated and fills whole of Current.
			-- (from EV_CONTAINER)
		require -- from EV_PIXMAPABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_PIXMAPABLE
			bridge_ok: (Result = Void and implementation.background_pixmap = Void) or (attached Result and then attached implementation.background_pixmap as l_pixmap and then Result.is_equal (l_pixmap))

	configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY]
			-- Agent used for customizing the Pick and Drop Target Menu of Current.
			-- (from EV_PICK_AND_DROPABLE)

	cursor: EV_DYNAMIC_LIST_CURSOR [EV_WIDGET]
			-- 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: detachable ANY
			-- Arbitrary user data may be stored here.
			-- (from EV_ANY)

	default_identifier_name: STRING_32
			-- Default name if no other name is set.
			-- (from EV_IDENTIFIABLE)
		ensure -- from EV_IDENTIFIABLE
			result_not_void: Result /= Void
			result_not_empty: not Result.is_empty
			no_period_in_result: not Result.has ('.'.to_character_32)

	default_key_processing_handler: detachable PREDICATE [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
			cursor_valid: (attached implementation.deny_cursor implies Result = implementation.deny_cursor) or else Result = Default_pixmaps.No_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)

	full_identifier_path: STRING_32
			-- Full name of object by prepending path of parent
			-- Uses '.' as a separator.
			-- (from EV_IDENTIFIABLE)
		ensure -- from EV_IDENTIFIABLE
			result_not_void: Result /= Void
			result_correct: parent = Void implies Result.is_equal (identifier_name)
			result_correct: attached parent as l_parent implies Result.is_equal (l_parent.full_identifier_path + ".".as_string_32 + identifier_name)

	generating_type: TYPE [detachable DV_HORIZONTAL_BOX]
			-- Type of current object
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty

	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

	has_recursive (an_item: like item): BOOLEAN
			-- Does structure include an_item or
			-- does any structure recursively included by structure,
			-- include an_item.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed

	help_context: detachable FUNCTION [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)
		require -- from READABLE_INDEXABLE
			valid_index: 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): detachable 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

	identifier_name: STRING_32
			-- Name of object
			-- If no specific name is set, `default_identifier_name` is used.
			-- (from EV_IDENTIFIABLE)
		ensure -- from EV_IDENTIFIABLE
			result_not_void: Result /= Void
			result_not_empty: not Result.is_empty
			no_period_in_result: not Result.has ('.'.to_character_32)
			default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name)

	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 ith 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)

	is_docking_enabled: BOOLEAN
			-- May Current be docked to?
			-- If True, Current will accept docking
			-- from a compatible EV_DOCKABLE_SOURCE.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			bridge_ok: Result = implementation.is_docking_enabled

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

	item_for_iteration: EV_WIDGET
			-- Item at current position
			-- (from LINEAR)
		require -- from LINEAR
			not_off: not off

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

	new_cursor: INDEXABLE_ITERATION_CURSOR [EV_WIDGET]
			-- Fresh cursor associated with current structure
			-- (from READABLE_INDEXABLE)
		require -- from  ITERABLE
			True
		ensure -- from ITERABLE
			result_attached: Result /= Void

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

	parent: detachable EV_CONTAINER
			-- Contains Current.
			-- (from EV_WIDGET)
		require -- from EV_IDENTIFIABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_IDENTIFIABLE
			correct: has_parent implies Result /= Void
			correct: not has_parent implies Result = Void
		ensure then -- from EV_WIDGET
			bridge_ok: Result = implementation.parent

	pebble: detachable 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: detachable FUNCTION [detachable 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

	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: detachable 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): detachable EV_WIDGET
			-- 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_WIDGET]
			-- 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

	target_data_function: detachable FUNCTION [like pebble, EV_PND_TARGET_DATA]
			-- Function for computing target meta data based on source pebble.
			-- Primarily used for Pick and Drop target menu.
			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
		note
			option: stable

	target_name: detachable READABLE_STRING_GENERAL
			-- Optional textual name describing Current pick and drop hole.
			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
		note
			option: stable

	veto_dock_function: detachable FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN]
			-- Function to determine whether current dock is allowed.
			-- If Result is True, dock will be disallowed.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			bridge_ok: Result = implementation.veto_dock_function
	
feature -- Measurement

	client_height: INTEGER_32
			-- Height of the area available to children in pixels.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			bridge_ok: Result = implementation.client_height

	client_width: INTEGER_32
			-- Width of the area available to children in pixels.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			bridge_ok: Result = implementation.client_width

	count: INTEGER_32
			-- Number of items.
			-- (from EV_DYNAMIC_LIST)
		require -- from  FINITE
			True
		require -- from  READABLE_INDEXABLE
			True
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from FINITE
			count_non_negative: Result >= 0
		ensure then -- from EV_DYNAMIC_LIST
			bridge_ok: Result = implementation.count

	dpi: NATURAL_32
			-- Window dpi
			-- (from EV_POSITIONED)
		require -- from EV_POSITIONED
			not_destroyed: not is_destroyed
		ensure -- from EV_POSITIONED
			positive_or_zero: Result >= 0

	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

	Lower: INTEGER_32 = 1
			-- Minimum index.
			-- (from CHAIN)

	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

	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 screen.
			-- (from EV_POSITIONED)
		require -- from EV_POSITIONED
			not_destroyed: not is_destroyed
		ensure -- from EV_POSITIONED
			bridge_ok: Result = implementation.screen_x

	screen_y: INTEGER_32
			-- Vertical offset relative to screen.
			-- (from EV_POSITIONED)
		require -- from EV_POSITIONED
			not_destroyed: not is_destroyed
		ensure -- from EV_POSITIONED
			bridge_ok: Result = implementation.screen_y

	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 -- Comparison

	frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			shallow_implies_deep: standard_equal (a, b) implies Result
			both_or_none_void: (a = Void) implies (Result = (b = Void))
			same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b))
			symmetric: Result implies deep_equal (b, a)

	frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b))

	frozen is_deep_equal alias "≡≡≡" (other: DV_HORIZONTAL_BOX): BOOLEAN
			-- Are Current and other attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)

	is_equal (other: DV_HORIZONTAL_BOX): BOOLEAN
			-- Does other contain the same elements?
			-- (from LIST)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			symmetric: Result implies other ~ 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 (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b 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
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b))

	frozen standard_is_equal alias "≜" (other: DV_HORIZONTAL_BOX): 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

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

	border_width: INTEGER_32
			-- Width of border around container in pixels.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			bridge_ok: Result = implementation.border_width
			positive: Result >= 0

	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

	debug_output: STRING_32
			-- String that should be displayed in debugger to represent Current.
			-- (from EV_IDENTIFIABLE)
		ensure -- from DEBUG_OUTPUT
			result_not_void: Result /= Void

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

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

	Full: BOOLEAN = 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

	has_identifier_name_set: BOOLEAN
			-- Is a specific identifier name set?
			-- (from EV_IDENTIFIABLE)

	has_parent: BOOLEAN
			-- Does identifiable has a parent?
			-- (from EV_IDENTIFIABLE)

	frozen id_freed: BOOLEAN
			-- Has Current been removed from the table?
			-- (from IDENTIFIED)

	is_default_non_expand: BOOLEAN
			-- Can't elements be expanded by default?
			-- (from DV_BOX)

	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_homogeneous: BOOLEAN
			-- Are all items forced to have same dimensions.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			bridge_ok: Result = implementation.is_homogeneous

	is_inserted (v: EV_WIDGET): 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_item_expanded (an_item: EV_WIDGET): BOOLEAN
			-- Is an_item expanded to occupy available spare space?
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			has_an_item: has (an_item)
		ensure -- from EV_BOX
			bridge_ok: Result = implementation.is_item_expanded (an_item)

	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

	merged_radio_button_groups: detachable ARRAYED_LIST [EV_CONTAINER]
			-- Result is all other radio button groups
			-- merged with Current. Void if no other containers
			-- are merged.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			not_is_empty: Result /= Void implies not Result.is_empty

	mode_is_configurable_target_menu: BOOLEAN
			-- Is the user interface mode a configurable 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_configurable_target_menu

	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

	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

	padding: INTEGER_32
			-- Space between children in pixels.
			-- Was declared in {EV_BOX} as synonym of `padding_width`.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			bridge_ok: Result = implementation.padding
			positive: Result >= 0

	padding_width: INTEGER_32
			-- Space between children in pixels.
			-- Was declared in {EV_BOX} as synonym of `padding`.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			bridge_ok: Result = implementation.padding
			positive: Result >= 0

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

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

	real_source: detachable 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

	replaceable: BOOLEAN
			-- Can current item be replaced?
			-- (from ACTIVE)

	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))

	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  READABLE_INDEXABLE
			True
		require -- from  TABLE
			True
		ensure -- from READABLE_INDEXABLE
			only_if_in_index_set: Result implies (Lower <= i and i <= count)
		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
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
	
feature -- Status setting

	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_borders
			-- Display without borders.
			-- (from DV_BOX)

	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_default_expand
			-- Disable default element displays expansion.
			-- (from DV_BOX)
		ensure -- from DV_BOX
			is_default_non_expand: is_default_non_expand

	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_docking
			-- Ensure `is_docking_enabled` is False.
			-- Current will not accept docking.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			not_dockable: not is_docking_enabled

	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_homogeneous
			-- Allow items to have different dimensions.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			not_is_homogeneous: not is_homogeneous

	disable_item_expand (an_item: EV_WIDGET)
			-- Do not expand an_item to occupy available spare space.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			has_an_item: has (an_item)
		ensure -- from EV_BOX
			not_an_item_expanded: not is_item_expanded (an_item)

	disable_padding
			-- Display without padding.
			-- (from DV_BOX)

	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_borders
			-- Display with borders.
			-- (from DV_BOX)

	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_default_expand
			-- Enable default element displays expansion.
			-- (from DV_BOX)
		ensure -- from DV_BOX
			is_default_expand: not is_default_non_expand

	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_docking
			-- Ensure `is_docking_enabled` is True.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			is_dockable: is_docking_enabled

	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_homogeneous
			-- Force all items to have same dimensions.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
		ensure -- from EV_BOX
			is_homogeneous: is_homogeneous

	enable_item_expand (an_item: EV_WIDGET)
			-- Expand an_item to occupy available spare space.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			has_an_item: has (an_item)
		ensure -- from EV_BOX
			an_item_expanded: is_item_expanded (an_item)

	enable_padding
			-- Display with padding.
			-- (from DV_BOX)

	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

	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

	merge_radio_button_groups (other: EV_CONTAINER)
			-- Merge Current radio button group with that of other.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
			other_not_void: other /= Void

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

	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

	set_accept_cursor (a_cursor: detachable 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)
		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
			accept_cursor_assigned: attached a_cursor as l_accept_cursor implies l_accept_cursor ~ accept_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_border_width (value: INTEGER_32)
			-- Assign value to `border_width`.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			positive_value: value >= 0
		ensure -- from EV_BOX
			border_width_assigned: border_width = value

	set_configurable_target_menu_handler (a_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY])
			-- Set Configurable Target Menu Handler to a_handler.
			-- (from EV_PICK_AND_DROPABLE)
		ensure -- from EV_PICK_AND_DROPABLE
			configurable_target_menu_hander_assigned: configurable_target_menu_handler = a_handler

	set_configurable_target_menu_mode
			-- Set user interface mode to pop-up menu of targets.
			-- Target menu is configurable as the first option can be used to
			-- initiate a regular 'pick and drop' of the source pebble.
			-- (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_configurable_target_menu

	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: detachable like deny_cursor)
			-- Set a_cursor to be displayed when the screen pointer is not
			-- over a valid target.
			-- (from EV_PICK_AND_DROPABLE)
		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
			deny_cursor_assigned: attached a_cursor as l_deny_cursor implies l_deny_cursor ~ deny_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 if `is_displayed`.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed
			is_sensitive: is_sensitive

	set_padding (value: INTEGER_32)
			-- Assign value to `padding_width`.
			-- Was declared in {EV_BOX} as synonym of `set_padding_width`.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			positive_value: value >= 0
		ensure -- from EV_BOX
			padding_assigned: padding = value

	set_padding_width (value: INTEGER_32)
			-- Assign value to `padding_width`.
			-- Was declared in {EV_BOX} as synonym of `set_padding`.
			-- (from EV_BOX)
		require -- from EV_BOX
			not_destroyed: not is_destroyed
			positive_value: value >= 0
		ensure -- from EV_BOX
			padding_assigned: padding = value

	set_pebble (a_pebble: ANY)
			-- 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 [detachable 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_data_function (a_function: FUNCTION [like pebble, EV_PND_TARGET_DATA])
			-- Set a_function to compute target meta data based on transport source.
			-- Overrides any `target_name` set with `set_target_name`.
			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
		require -- from EV_ABSTRACT_PICK_AND_DROPABLE
			a_function_not_void: a_function /= Void
		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
			target_data_function_assigned: target_data_function /= Void and then target_data_function.is_equal (a_function)

	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: READABLE_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: attached target_name as l_target_name and then a_name /= l_target_name and then a_name.same_string (l_target_name)

	set_veto_dock_function (a_function: FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN])
			-- Assign a_function to `veto_dock_function`.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
			a_function_not_void: a_function /= Void
		ensure -- from EV_DOCKABLE_TARGET
			veto_function_set: veto_dock_function = a_function

	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_configurable_target_menu (a_x, a_y: INTEGER_32)
			-- Show the configurable target menu at position a_x, a_y relative to Current.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from EV_PICK_AND_DROPABLE
			not_destroyed: not is_destroyed
			mode_is_configurable_target_menu: mode_is_configurable_target_menu
			configurable_menu_handler_set: configurable_target_menu_handler /= Void

	unmerge_radio_button_groups (other: EV_CONTAINER)
			-- Remove other from radio button group of Current.
			-- If no radio button of other was checked before removal
			-- then first radio button contained will be checked.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
			other_is_merged: attached merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_groups.has (other)
		ensure -- from EV_CONTAINER
			other_not_merged: other.merged_radio_button_groups = Void
			not_contained_in_this_group: attached merged_radio_button_groups as l_merged_r_b_groups implies not l_merged_r_b_groups.has (other)
			other_first_radio_button_now_selected: not old other.has_selected_radio_button and old other.has_radio_button implies other.first_radio_button_selected
			original_radio_button_still_selected: old has_selected_radio_button implies has_selected_radio_button
			other_first_radio_button_now_selected: not old has_selected_radio_button and old other.has_radio_button and (attached old merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_groups.count = 1) and has_radio_button implies first_radio_button_selected
			other_original_radio_button_still_selected: old other.has_selected_radio_button implies other.has_selected_radio_button
	
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 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_WIDGET])
			-- 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: DV_HORIZONTAL_BOX)
			-- 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: DV_HORIZONTAL_BOX)
			-- 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 EV_CONTAINER
			not_destroyed: not is_destroyed
			writable: writable
			v_not_void: v /= Void
			v_parent_void: v.parent = Void
			v_not_current: v /= Current
			v_not_parent_of_current: not is_parent_recursive (v)
			v_containable: may_contain (v)
		require -- from CHAIN
			writeable: writable
			replaceable: replaceable
		ensure -- from EV_CONTAINER
			has_v: has (v)
			not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has (l_item))
		ensure -- from CHAIN
			same_count: count = old count
			is_inserted: is_inserted (v)

	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_background_pixmap
			-- Remove image displayed on Current.
			-- (from EV_PIXMAPABLE)
		require -- from EV_PIXMAPABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_PIXMAPABLE
			pixmap_removed: background_pixmap = Void

	replace (v: like item)
			-- Replace current item by v.
			-- (from EV_DYNAMIC_LIST)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
			writable: writable
			v_not_void: v /= Void
			v_parent_void: v.parent = Void
			v_not_current: v /= Current
			v_not_parent_of_current: not is_parent_recursive (v)
			v_containable: may_contain (v)
		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_CONTAINER
			has_v: has (v)
			not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has (l_item))
		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

	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_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: FUNCTION [EV_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: attached help_context as l_help_context and then l_help_context.is_equal (an_help_context)

	set_identifier_name (a_name: READABLE_STRING_GENERAL)
			-- Set `identifier_name` to a_name.
			-- (from EV_IDENTIFIABLE)
		require -- from EV_IDENTIFIABLE
			a_name_not_void: a_name /= Void
			a_name_not_empty: not a_name.is_empty
			no_period_in_name: not a_name.has ('.'.to_character_32)
			no_special_regexp_characters_in_name: 
		ensure -- from EV_IDENTIFIABLE
			identifier_name_set: identifier_name.same_string_general (a_name)

	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: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1))
			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: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1))
			minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1))
			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: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1))
			minimum_width_set_by_user_set: minimum_width_set_by_user

	set_background_pixmap (a_pixmap: EV_PIXMAP)
			-- Display image of a_pixmap on Current.
			-- Image of pixmap will be a copy of a_pixmap.
			-- Image may be scaled in some descendents, i.e EV_TREE_ITEM
			-- See EV_TREE.set_pixmaps_size.
			-- (from EV_PIXMAPABLE)
		require -- from EV_PIXMAPABLE
			not_destroyed: not is_destroyed
			pixmap_not_void: a_pixmap /= Void

	set_pointer_style (a_cursor: EV_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: attached pointer_style as l_pointer_style and then l_pointer_style.is_equal (a_cursor)

	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

	dispose
			-- Free the entry associated with `object_id` if any
			-- (from IDENTIFIED)
		require -- from  DISPOSABLE
			True
		ensure then -- from IDENTIFIED
			object_freed: id_freed

	frozen free_id
			-- Free the entry associated with `object_id` if any.
			-- (from IDENTIFIED)
		ensure -- from IDENTIFIED
			object_freed: id_freed

	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 EV_CONTAINER
			not_destroyed: not is_destroyed
			writable: prunable
			v_not_void: v /= Void
			v_parent_void: v.parent = Current
			v_not_current: v /= Current
		ensure -- from EV_CONTAINER
			has_v: 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 /= Void and then 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_i_th (i: INTEGER_32)
			-- Remove item at index i.
			-- Move cursor to next neighbor (or `after` if no next neighbor) if it is at i-th position.
			-- Do not change cursor otherwise.
			-- (from DYNAMIC_CHAIN)
		require -- from DYNAMIC_TABLE
			prunable: prunable
			valid_key: valid_index (i)
		ensure then -- from DYNAMIC_CHAIN
			new_count: count = old count - 1
			same_index_if_below: index <= i implies index = old index
			new_index_if_above: index > i implies index = old index - 1
			same_leading_items: ∀ c: old twin ¦
@					c.target_index < i implies c = i_th (.target_index)
			same_trailing_items: ∀ c: old twin ¦
					.target_index > i implies c = i_th (.target_index - 1)

	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

	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_WIDGET]
			-- Representation as a linear structure
			-- (from LINEAR)
		require -- from  CONTAINER
			True
	
feature -- Duplication

	frozen deep_copy (other: DV_HORIZONTAL_BOX)
			-- 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: DV_HORIZONTAL_BOX
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		ensure -- from ANY
			deep_twin_not_void: Result /= Void
			deep_equal: deep_equal (Current, Result)

	frozen standard_copy (other: DV_HORIZONTAL_BOX)
			-- 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: DV_HORIZONTAL_BOX
			-- 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: DV_HORIZONTAL_BOX
			-- New object equal to Current
			-- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`.
			-- (from ANY)
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result ~ Current
	
feature -- Basic operations

	frozen default: detachable DV_HORIZONTAL_BOX
			-- 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)
		ensure -- from ANY
			instance_free: class

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

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class

	extend (widget: EV_WIDGET)
			-- Add widget to end of structure.
			-- (from DV_BOX)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
			extendible: extendible
			v_not_void: widget /= Void
			v_parent_void: widget.parent = Void
			v_not_current: widget /= Current
			v_not_parent_of_current: not is_parent_recursive (widget)
			v_containable: may_contain (widget)
		require -- from EV_DYNAMIC_LIST
			not_destroyed: not is_destroyed
			extendible: extendible
			v_not_void: widget /= Void
			v_parent_void: widget.parent = Void
			v_not_current: not same (widget)
			v_not_parent_of_current: not is_parent_recursive (widget)
		ensure -- from EV_CONTAINER
			has_v: has (widget)
		ensure -- from EV_DYNAMIC_LIST
			parent_is_current: widget.parent = Current
			v_is_last: widget = last
			count_increased: count = old count + 1
			cursor_not_moved: (index = old index) or (after and old after)

	extend_cell
			-- Add a cell, i.e. an empty display element,
			-- to end of structure.
			-- (from DV_BOX)

	extend_separator
			-- Add a non-expandable separator to end
			-- of structure.

	propagate_background_color
			-- Propagate `background_color` recursively, to all children.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			background_color_propagated: background_color_propagated

	propagate_foreground_color
			-- Propagate `foreground_color` recursively, to all children.
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			foreground_color_propagated: foreground_color_propagated

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

	set_default_border_width (new_border_width: INTEGER_32)
			-- Set new_border_width as default border width.
			-- (from DV_BOX)

	set_default_padding (new_padding: INTEGER_32)
			-- Set new_padding as default padding.
			-- (from DV_BOX)
	
feature -- Inapplicable

	dl_append (s: SEQUENCE [EV_WIDGET])
			-- Append a copy of s.
			-- (from EV_DYNAMIC_LIST)
		require -- from SEQUENCE
			argument_not_void: s /= Void
		ensure -- from SEQUENCE
			new_count: count >= old count

	dl_put_front (v: like item)
			-- Add v at beginning.
			-- Do not move cursor.
			-- (from EV_DYNAMIC_LIST)
		require -- from DYNAMIC_CHAIN
			extendible: extendible
		ensure -- from DYNAMIC_CHAIN
			new_count: count = old count + 1
			item_inserted: first = v

	dl_put_i_th (v: like item; i: INTEGER_32)
			-- Put v at i-th position.
			-- (from EV_DYNAMIC_LIST)
		require -- from TABLE
			valid_key: valid_index (i)
		require -- from TABLE
			valid_key: valid_index (i)
		ensure -- from TABLE
			inserted: i_th (i) = v

	dl_put_left (v: like item)
			-- Add v to the left of cursor position.
			-- Do not move cursor.
			-- (from EV_DYNAMIC_LIST)
		require -- from DYNAMIC_CHAIN
			extendible: extendible
			not_before: not before
		ensure -- from DYNAMIC_CHAIN
			new_count: count = old count + 1
			new_index: index = old index + 1

	dl_put_right (v: like item)
			-- Add v to the right of cursor position.
			-- Do not move cursor.
			-- (from EV_DYNAMIC_LIST)
		require -- from DYNAMIC_CHAIN
			extendible: extendible
			not_after: not after
		ensure -- from DYNAMIC_CHAIN
			new_count: count = old count + 1
			same_index: index = old index

	dl_replace (v: like item)
			-- Replace current item by v.
			-- (from EV_DYNAMIC_LIST)
		require -- from ACTIVE
			writable: writable
			replaceable: replaceable
		ensure -- from ACTIVE
			item_replaced: item = v
	
feature -- Implementation

	Changeable_comparison_criterion: BOOLEAN = False
			-- May `object_comparison` be changed?
			-- (Answer: no by default.)
			-- (from EV_CONTAINER)

	cl_extend (v: like item)
			-- Ensure that structure includes v.
			-- (from EV_CONTAINER)
		require -- from COLLECTION
			extendible: extendible
		ensure -- from COLLECTION
			item_inserted: is_inserted (v)

	cl_prune (v: like item)
			-- Remove one occurrence of v if any.
			-- (Reference or object equality,
			-- based on `object_comparison`.)
			-- (from EV_CONTAINER)
		require -- from COLLECTION
			prunable: prunable

	cl_put (v: like item)
			-- Replace `item` with v.
			-- (from EV_CONTAINER)
		require -- from COLLECTION
			extendible: extendible
		ensure -- from COLLECTION
			item_inserted: is_inserted (v)
		ensure then -- from SEQUENCE
			new_count: count = old count + 1
	
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_background_color_void: BOOLEAN
			-- If `background_color` void?
			-- (from EV_COLORIZABLE)

	is_foreground_color_void: BOOLEAN
			-- If `foreground_color` void?
			-- (from EV_COLORIZABLE)

	is_in_default_state: BOOLEAN
			-- Is Current in its default state.
			-- (from EV_BOX)
		require -- from  EV_ANY
			True

	is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
			-- Is a_widget `parent`, or recursivly, `parent` of `parent`.
			-- (from EV_CONTAINER)
		require -- from EV_DYNAMIC_LIST
			a_list_not_void: a_widget /= Void
			not_destroyed: not is_destroyed
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed

	may_contain (v: EV_WIDGET): BOOLEAN
			-- May v be inserted in Current.
			-- Instances of EV_WINDOW may not be inserted
			-- in a container even though they are widgets.
			-- (from EV_CONTAINER)

	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 -- Event handling

	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

	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

	docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE
			-- Actions to be performed when a dockable source completes a transport
			-- Fired only if source has been moved, after parenting.
			-- (from EV_DOCKABLE_TARGET_ACTION_SEQUENCES)
		ensure -- from EV_DOCKABLE_TARGET_ACTION_SEQUENCES
			not_void: Result /= Void

	dpi_changed_actions: EV_DPI_ACTION_SEQUENCE
			-- Actions to be performed when size changes.
			-- (from EV_WIDGET_ACTION_SEQUENCES)
		ensure -- from EV_WIDGET_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

	file_drop_actions: EV_LITE_ACTION_SEQUENCE [LIST [STRING_32]]
			-- Actions to be performed when an OS file drop is performed on Current.
			-- (from EV_WIDGET_ACTION_SEQUENCES)

	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
	
feature -- Iteration

	do_all (action: PROCEDURE [EV_WIDGET])
			-- 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 [EV_WIDGET]; test: FUNCTION [EV_WIDGET, 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_exists: test /= Void

	for_all (test: FUNCTION [EV_WIDGET, 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_exists: test /= Void
		ensure then -- from LINEAR
			empty: is_empty implies Result

	there_exists (test: FUNCTION [EV_WIDGET, 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_exists: test /= Void
	
feature -- Output

	Io: STD_FILES
			-- Handle to standard file setup
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			io_not_void: Result /= Void

	out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		ensure -- from ANY
			out_not_void: Result /= Void

	print (o: detachable ANY)
			-- Write terse external representation of o
			-- on standard output.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class

	frozen tagged_out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		ensure -- from ANY
			tagged_out_not_void: Result /= Void
	
feature -- Platform

	Operating_environment: OPERATING_ENVIRONMENT
			-- Objects available from the operating system
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			operating_environment_not_void: Result /= Void
	
feature -- Status Report

	is_destroyed: BOOLEAN
			-- Is Current no longer usable?
			-- (from EV_ANY)
		ensure -- from EV_ANY
			bridge_ok: Result = implementation.is_destroyed
	
invariant
		-- from EV_CONTAINER
	client_width_non_negative: is_usable implies client_width >= 0
	client_width_within_limit: is_usable implies client_width <= width
	client_height_non_negative: is_usable implies client_height >= 0
	client_height_within_limit: is_usable implies client_height <= height
	all_radio_buttons_connected: is_usable implies all_radio_buttons_connected
	parent_of_items_is_current: is_usable implies parent_of_items_is_current
	items_unique: is_usable implies items_unique

		-- from EV_WIDGET
	is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested
	parent_contains_current: is_usable and then attached parent as l_parent implies l_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
	default_create_called: default_create_called
	is_coupled: default_create_called implies (implementation.interface = Current or (attached {EV_ENVIRONMENT} Current and then attached implementation.interface))

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

		-- 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_DOCKABLE_SOURCE
	parent_permits_docking: is_dockable implies parent_of_source_allows_docking

		-- from EV_COLORIZABLE
	background_color_not_void: is_usable implies not is_background_color_void
	foreground_color_not_void: is_usable implies not is_foreground_color_void

		-- 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))

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

		-- from READABLE_INDEXABLE
	consistent_boundaries: Lower <= count or else Lower = count + 1

		-- 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)

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 -- class DV_HORIZONTAL_BOX


Classes
Clusters
Cluster hierarchy
Chart
Relations
Flat contracts
Go to: