    indexing
    	description: "[
    		An EV_FIGURE_WORLD_CELL is an EV_CELL with scrollbars displaying
    		world in the cell. Whenever the world does not fit into the frame
    		the scrolling area is resized to make sure that every part of the world
    		is reachable through the scrollbars. If a figure is moved closer to the
    		frame border then autoscroll_border the frame starts to scroll.
    		If the user clicks into the frame but not onto a figure the frame can
    		be moved arround with the "hand". A buffer is used to prefend flickering.
    		The buffer size as well as the drawing_area size is constant no matter
    		how large the world is.

    		example:

    			create figure_world_cell.make_with_world (create EV_FIGURE_WORLD)
    			figure_world_cell.world.extend (create {EV_FIGURE_LINE}.make_with_positions (0, 0, 100, 100))
    			horizontal_box.extend (figure_world_cell)

    	]"
    	legal: "See notice at end of class."
    	status: "See notice at end of class."
    	date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
    	revision: "$Revision: 56675 $"

    class interface
    	EV_MODEL_WORLD_CELL

    create
    	make_with_world (a_world: like world)
    			-- Create an EV_FIGURE_WORLD_FRAM displaying `a_world'.
    		require
    			a_world_not_void: a_world /= Void
    		ensure
    			world_set: world = a_world

    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

    	autoscroll_border: INTEGER_32
    			-- Distance to the frame border wher scrolling starts.

    	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: 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 Result.is_equal (implementation.background_pixmap)

    	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

    	drawing_area: EV_DRAWING_AREA
    			-- Graphical surface displaying world.

    	ev_application: EV_APPLICATION
    			-- Current application. This once feature must be called
    			-- only if the application has been created
    			-- (from EV_SHARED_APPLICATION)
    		ensure -- from EV_SHARED_APPLICATION
    			result_not_void: Result /= Void

    	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: EV_WIDGET): BOOLEAN
    			-- Does `Current' include `v'?
    			-- (from EV_CELL)
    		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: 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

    	horizontal_scrollbar: EV_HORIZONTAL_SCROLL_BAR
    			-- Horizontal scroll bar.

    	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

    	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
    			-- Current item.
    			-- (from EV_CONTAINER)
    		require -- from EV_CONTAINER
    			not_destroyed: not is_destroyed
    			readable: readable
    		ensure -- from EV_CONTAINER
    			bridge_ok: Result = implementation.item

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

    	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

    	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

    	process_events_and_idle
    			-- Call `process_events' and `idle_actions' on Ev_application.
    			-- (from EV_SHARED_APPLICATION)

    	projector: EV_MODEL_BUFFER_PROJECTOR
    			-- Projector to render world.

    	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

    	scroll_speed: REAL_64
    			-- Speed of auto scroll. Autoscroll happens every 50 milliseconds for
    			-- scroll_speed * (distance between autoscroll_border and cursor)
    			-- Pixels. Meaning the nearer the cursor is to the cell border the
    			-- faster the scroll plus the higher the scroll_speed value the faster
    			-- the scroll. Default is 1.0.

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

    	vertical_scrollbar: EV_VERTICAL_SCROLL_BAR
    			-- Vertical scroll bar.

    	veto_dock_function: FUNCTION [ANY, TUPLE [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

    	world: EV_MODEL_WORLD
    			-- The world shown in `Current'.

    	world_border: INTEGER_32
    			-- Minimal distance between world borders and frame borders.

    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

    	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
    			-- Is `other' attached to an object considered
    			-- equal to current object?
    			-- (from ANY)
    		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

    	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

    	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

    	count: INTEGER_32
    			-- Number of items in `Current'.
    			-- (from EV_CELL)
    		require -- from EV_CONTAINER
    			not_destroyed: not is_destroyed
    		ensure then -- from EV_CELL
    			valid_result: Result = 0 or Result = 1

    	extendible: BOOLEAN
    			-- Is there no element?
    			-- Was declared in EV_CELL as synonym of is_empty.
    			-- (from EV_CELL)

    	full: BOOLEAN
    			-- Is structure filled to capacity?
    			-- (from EV_CELL)

    	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

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

    	is_autoscroll_enabled: BOOLEAN
    			-- Is autoscroll enabled?

    	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 there no element?
    			-- Was declared in EV_CELL as synonym of extendible.
    			-- (from EV_CELL)

    	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_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_resize_enabled: BOOLEAN
    			-- Is resizing enabled?

    	is_scrollbar_enabled: BOOLEAN
    			-- Are scrollbars visible?

    	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

    	merged_radio_button_groups: 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_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

    	prunable: BOOLEAN
    			-- May items be removed?
    			-- (from EV_CELL)

    	readable: BOOLEAN
    			-- Is there a current item that may be accessed?
    			-- (from EV_CELL)
    		require -- from EV_CONTAINER
    			not_destroyed: not is_destroyed

    	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

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

    	writable: BOOLEAN
    			-- Is there a current item that may be modified?
    			-- (from EV_CELL)
    		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

    	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_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_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_resize
    			-- Set is_resize_enabled to False.
    		ensure
    			set: is_resize_enabled = False

    	disable_scrollbars
    			-- Hide scrollbars.
    		ensure
    			hide: not horizontal_scrollbar.is_show_requested and not vertical_scrollbar.is_show_requested
    			set: not is_scrollbar_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_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_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_resize
    			-- Set is_resize_enabled to True.
    		ensure
    			set: is_resize_enabled = True

    	enable_scrollbars
    			-- Show scrollbars.
    		ensure
    			show: horizontal_scrollbar.is_show_requested and vertical_scrollbar.is_show_requested
    			set: is_scrollbar_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
    		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

    	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)

    	set_veto_dock_function (a_function: FUNCTION [ANY, TUPLE [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

    	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: merged_radio_button_groups.has (other)
    		ensure -- from EV_CONTAINER
    			other_not_merged: other.merged_radio_button_groups = Void
    			not_contained_in_this_group: merged_radio_button_groups /= Void implies not merged_radio_button_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 old merged_radio_button_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 -- Element change

    	crop
    			-- Resize Scrollbars such that world plus world_border plus autoscroll_border fits in cell.

    	cut
    			-- Resize scrollbars such that there is no overhang (crop without scrolling).

    	extend (v: like item)
    			-- Ensure that structure includes `v'.
    			-- Do not move cursor.
    			-- (from EV_CONTAINER)
    		require -- from EV_CONTAINER
    			not_destroyed: not is_destroyed
    			extendible: extendible
    			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)
    		ensure -- from EV_CONTAINER
    			has_v: has (v)

    	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 COLLECTION)
    		require -- from COLLECTION
    			other_not_void: other /= Void
    			extendible: extendible

    	fit_to_screen
    			-- Zoom world such that it fits to screen.

    	put (v: like item)
    			-- Replace item with `v'.
    			-- Was declared in EV_CONTAINER as synonym of replace.
    			-- (from EV_CONTAINER)
    		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)
    		ensure -- from EV_CONTAINER
    			has_v: has (v)
    			not_has_old_item: not has (old item)

    	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 item with `v'.
    			-- Was declared in EV_CONTAINER as synonym of put.
    			-- (from EV_CONTAINER)
    		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)
    		ensure -- from EV_CONTAINER
    			has_v: has (v)
    			not_has_old_item: not has (old item)

    	set_autoscroll_border (a_border: like autoscroll_border)
    			-- Set autoscroll_border to `a_border'.
    		require
    			a_border_positive: a_border >= 0
    		ensure
    			set: autoscroll_border = a_border

    	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: 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_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: 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_scroll_speed (a_scroll_speed: like scroll_speed)
    			-- Set scroll_speed to `a_scroll_speed'.
    		require
    			a_scroll_speed_positive: a_scroll_speed >= 0.0
    		ensure
    			set: scroll_speed = a_scroll_speed

    	set_world (a_world: like world)
    			-- Set world to `a_world'.
    		require
    			a_world_not_void: a_world /= Void
    		ensure
    			set: world = a_world

    	set_world_border (a_border: like world_border)
    			-- Set world_border to `a_border'.
    		require
    			a_border_positive: a_border >= 0
    		ensure
    			set: world_border = a_border

    feature -- Removal

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

    	prune (v: EV_WIDGET)
    			-- Remove `v' if contained.
    			-- (from EV_CELL)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure then -- from EV_CELL
    			not has (v)

    	prune_all (v: EV_WIDGET)
    			-- Remove all occurrences of `v'.
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from COLLECTION)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure -- from COLLECTION
    			no_more_occurrences: not has (v)

    	wipe_out
    			-- Remove item.
    			-- (from EV_CELL)
    		require -- from COLLECTION
    			prunable: prunable
    		ensure -- from COLLECTION
    			wiped_out: is_empty

    feature -- Conversion

    	linear_representation: LINEAR [like item]
    			-- Representation as a linear structure
    			-- (from EV_CELL)

    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)

    	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

    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_widget: EV_WIDGET): BOOLEAN
    			-- Is `a_widget' parent, or recursivly, parent of parent.
    			-- (from EV_CONTAINER)
    		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)

    	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

    	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

    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 -- Status Report

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

    invariant
    	scroll_speed_positive: scroll_speed >= 0.0

    		-- from EV_CONTAINER
    	client_width_within_bounds: is_usable implies client_width >= 0 and client_width <= width
    	client_height_within_bounds: is_usable implies client_height >= 0 and 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
    	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

    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_MODEL_WORLD_CELL