indexing
	description: "Eiffel Vision window. Implementation interface."
	legal: "See notice at end of class."
	status: "See notice at end of class."
	date: "$Date: 2007-02-23 12:08:55 -0800 (Fri, 23 Feb 2007) $"
	revision: "$Revision: 66878 $"

deferred class interface
	EV_WINDOW_I


feature -- Access

	accelerator_list: EV_ACCELERATOR_LIST
			-- Key combination shortcuts associated with this window.

	accept_cursor: EV_POINTER_STYLE
			-- Accept cursor set by user.
			-- To be displayed when the screen pointer is over a target that accepts
			-- pebble during pick and drop.
			-- (from EV_PICK_AND_DROPABLE_I)

	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', will use the default drop target.
			-- Always void if `Current' is not a widget.
			-- (from EV_WIDGET_I)

	background_color: EV_COLOR
			-- Color displayed behind foregournd features.
			-- (from EV_COLORIZABLE_I)

	client_height: INTEGER_32
			-- Height of the client area of container.
			-- (from EV_CONTAINER_I)
		ensure -- from EV_CONTAINER_I
			positive: Result >= 0

	client_width: INTEGER_32
			-- Width of the client area of container.
			-- (from EV_CONTAINER_I)
		ensure -- from EV_CONTAINER_I
			positive: Result >= 0

	configurable_target_menu_handler: PROCEDURE [ANY, TUPLE [menu: EV_MENU; target_list: ARRAYED_LIST [EV_PND_TARGET_DATA]; source: EV_PICK_AND_DROPABLE; source_pebble: ANY]]
			-- (from EV_PICK_AND_DROPABLE_I)

	default_key_processing_handler: PREDICATE [ANY, TUPLE [EV_KEY]]
			-- 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 occuring.
			-- (from EV_WIDGET_I)

	deny_cursor: EV_POINTER_STYLE
			-- Deny cursor set by user.
			-- To be displayed when the screen pointer is not over a valid target.
			-- (from EV_PICK_AND_DROPABLE_I)

	foreground_color: EV_COLOR
			-- Color of foreground features like text.
			-- (from EV_COLORIZABLE_I)

	generating_type: STRING_8
			-- Name of current object's generating type
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void
			generating_type_not_empty: not Result.is_empty

	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 structure include `v'?

	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_I)
		ensure -- from EV_HELP_CONTEXTABLE_I
			current_if_exists: internal_help_context /= Void implies Result = internal_help_context

	internal_maximum_height: INTEGER_32
			-- Maximum height that `Current' can take.

	internal_maximum_width: INTEGER_32
			-- Maximum width that `Current' can take.

	internal_pointer_style: EV_POINTER_STYLE
			-- Cursor displayed when screen pointer is over current widget,
			-- as seen from interface.
			-- (from EV_WIDGET_I)

	is_border_enabled: BOOLEAN
			-- Is a border displayed around `Current'?
			-- Always return `True' if user_can_resize.

	is_dock_executing: BOOLEAN
			-- Is `Current' in the process of a dockable transport?
			-- (from EV_DOCKABLE_SOURCE_I)

	is_dockable: BOOLEAN
			-- Is `Current' dockable?
			-- (from EV_DOCKABLE_SOURCE_I)

	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 the transport?
			-- (from EV_DOCKABLE_SOURCE_I)

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

	item: EV_WIDGET
			-- Current item.
			-- (from EV_CONTAINER_I)

	lower_bar: EV_VERTICAL_BOX
			-- Room at bottom of `Current'. (Example use: statusbar.)

	maximum_height: INTEGER_32
			-- Maximum height that `Current' can take.

	maximum_width: INTEGER_32
			-- Maximum width that `Current' can take.

	menu_bar: EV_MENU_BAR
			-- Horizontal bar at top of client area that contains menu's.

	merged_radio_button_groups: ARRAYED_LIST [EV_CONTAINER]
			-- `Result' is all other radio button groups
			-- merged with `Current'.
			-- (from EV_CONTAINER_I)
		ensure -- from EV_CONTAINER_I
			current_not_included: Result /= Void implies not Result.has (interface)

	not_external_docking_enabled: BOOLEAN
			-- Attribute used for `is_externally_dockable'. We must implement
			-- `is_externally_dockable' this way as we have no easy solution to
			-- assign `True' to `is_externally_dockable'.
			-- (from EV_DOCKABLE_SOURCE_I)

	not_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.
			-- Internal reversed value of is_external_docking_relative as we cannot
			-- easily initialize a BOOLE to True in this case.
			-- (from EV_DOCKABLE_SOURCE_I)

	original_parent_position: INTEGER_32
			-- Original position in parent. Required
			-- to restore widget later.
			-- (from EV_DOCKABLE_SOURCE_I)

	parent: EV_CONTAINER
			-- Container widget that contains `Current'.
			-- (Void if `Current' is not in a container)
			-- (from EV_WIDGET_I)

	pebble: ANY
			-- Data to be transported by pick and drop mechanism.
			-- (from EV_PICK_AND_DROPABLE_I)

	pebble_function: FUNCTION [ANY, TUPLE, ANY]
			-- Returns data to be transported by pick and drop mechanism.
			-- (from EV_PICK_AND_DROPABLE_I)

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

	pebble_x_position: INTEGER_32
			-- Initial x position for pick and drop relative to `Current'.
			-- (from EV_PICK_AND_DROPABLE_I)

	pebble_y_position: INTEGER_32
			-- Initial y position for pick and drop relative to `Current'.
			-- (from EV_PICK_AND_DROPABLE_I)

	background_pixmap: EV_PIXMAP
			-- Image displayed on `Current'.
			-- (from EV_PIXMAPABLE_I)

	pointer_position: EV_COORDINATE
			-- Position of the screen pointer relative to `Current'.
			-- (from EV_WIDGET_I)
		ensure -- from EV_WIDGET_I
			result_not_void: Result /= Void

	pointer_style: EV_POINTER_STYLE
			-- Cursor displayed when screen pointer is over current widget.
			-- Void if none has been set using `set_pointer_position'.
			-- (from EV_WIDGET_I)

	real_source: EV_DOCKABLE_SOURCE
			-- `Result' is EV_DOCKABLE_SOURCE which should be
			-- dragged when docking begins on `Current'.
			-- (from EV_DOCKABLE_SOURCE_I)

	real_target: EV_DOCKABLE_TARGET
			-- `Result' is target used during a dockable transport if
			-- mouse pointer is above `Current'.
			-- (from EV_WIDGET_I)

	title: STRING_32
			-- Application name to be displayed by the window manager.

	upper_bar: EV_VERTICAL_BOX
			-- Room at top of `Current'. (Example use: toolbars.)
			-- Positioned below menu bar.

	user_can_resize: BOOLEAN
			-- Can the user resize?
	
feature -- Measurement

	height: INTEGER_32
			-- Vertical size in pixels.
			-- (from EV_POSITIONED_I)

	minimum_height: INTEGER_32
			-- Minimum vertical size in pixels.
			-- (from EV_POSITIONED_I)

	minimum_width: INTEGER_32
			-- Minimum horizontal size in pixels.
			-- (from EV_POSITIONED_I)

	screen_x: INTEGER_32
			-- Horizontal offset relative to screen.
			-- (from EV_WIDGET_I)
		require -- from  EV_POSITIONED_I
			True

	screen_y: INTEGER_32
			-- Vertical offset relative to screen.
			-- (from EV_WIDGET_I)
		require -- from  EV_POSITIONED_I
			True

	width: INTEGER_32
			-- Horizontal size in pixels.
			-- (from EV_POSITIONED_I)

	x_position: INTEGER_32
			-- Horizontal offset relative to parent x_position in pixels.
			-- (from EV_POSITIONED_I)

	y_position: INTEGER_32
			-- Vertical offset relative to parent y_position in pixels.
			-- (from EV_POSITIONED_I)
	
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 (other /= Void and then 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))

	frozen is_deep_equal (other: EV_WINDOW_I): 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: EV_WINDOW_I): 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: EV_WINDOW_I): 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

	closest_dockable_target: EV_DOCKABLE_TARGET
			-- `Result' is first dockable target that is_dockable found by recursively
			-- searching up through the parenting structure from the widget
			-- currently underneath the pointer position.
			-- `Result' will be `Void' if a dockable target is not found.
			-- (from EV_DOCKABLE_SOURCE_I)
		ensure -- from EV_DOCKABLE_SOURCE_I
			result_is_dockable: Result /= Void implies Result.is_docking_enabled

	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

	get_next_target (a_widget: EV_WIDGET): EV_DOCKABLE_TARGET
			-- `Result' is next dockable target that is is_dockable found by
			-- recursively seraching up the parenting structure from `current_target'.
			-- `Result' will be `Void' if none.
			-- (from EV_DOCKABLE_SOURCE_I)
		require -- from EV_DOCKABLE_SOURCE_I
			a_widget_not_void: a_widget /= Void
		ensure -- from EV_DOCKABLE_SOURCE_I
			result_is_dockable: Result /= Void implies Result.is_docking_enabled

	internal_non_sensitive: BOOLEAN
			-- Is `Current' not sensitive to input as seen
			-- from interface?
			-- (from EV_SENSITIVE_I)

	is_destroyed: BOOLEAN
			-- Is `Current' no longer usable?
			-- (from EV_ANY_I)

	is_docking_enabled: BOOLEAN
			-- May `Current' be docked to?
			-- (from EV_DOCKABLE_TARGET_I)

	is_transport_enabled: BOOLEAN
			-- Is the transport mechanism enabled?
			-- (from EV_PICK_AND_DROPABLE_I)

	mode_is_configurable_target_menu: BOOLEAN
			-- Is the transport mechanism a configurable target menu?
			-- (from EV_PICK_AND_DROPABLE_I)

	mode_is_drag_and_drop: BOOLEAN
			-- Is the transport mechanism drag and drop?
			-- (from EV_PICK_AND_DROPABLE_I)

	mode_is_pick_and_drop: BOOLEAN
			-- Is the transport mechanism pick and drop?
			-- (from EV_PICK_AND_DROPABLE_I)

	mode_is_target_menu: BOOLEAN
			-- Is the transport mechanism a target menu?
			-- (from EV_PICK_AND_DROPABLE_I)

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

	user_is_sensitive: BOOLEAN
			-- Is the object sensitive to user input.
			-- (from EV_SENSITIVE_I)

	veto_dock_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN]
			-- Function used to veto transport.
			-- (from EV_DOCKABLE_TARGET_I)
	
feature -- Status setting

	allow_resize
			-- Allow the resize of the window.

	disable_border
			-- Ensure no border is displayed around `Current'
			-- and set internal_is_border_enabled to `False'.
		ensure
			border_disabled: not user_can_resize implies not is_border_enabled

	disable_dockable
			-- Ensure `Current' is not dockable
			-- (from EV_DOCKABLE_SOURCE_I)
		ensure -- from EV_DOCKABLE_SOURCE_I
			not_is_dockable: not is_dockable

	disable_docking
			-- Ensure is_docking_enabled is False.
			-- `Current' will not accept docking.
			-- (from EV_DOCKABLE_TARGET_I)
		ensure -- from EV_DOCKABLE_TARGET_I
			not_dockable: not is_docking_enabled
			id_not_stored_in_application: not (create {EV_ENVIRONMENT}).application.implementation.dockable_targets.has (interface.object_id)

	disable_external_docking
			-- Forbid `Current' to be docked into an EV_DOCKABLE_DIALOG
			-- When there is no valid EV_DRAGABLE_TARGET upon completion
			-- of the transport?
			-- (from EV_DOCKABLE_SOURCE_I)
		require -- from EV_DOCKABLE_SOURCE_I
			is_dockable: is_dockable
		ensure -- from EV_DOCKABLE_SOURCE_I
			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_I)
		require -- from EV_DOCKABLE_SOURCE_I
			external_docking_enabled: is_external_docking_enabled
		ensure -- from EV_DOCKABLE_SOURCE_I
			external_docking_not_relative: not is_external_docking_relative

	disable_pebble_positioning
			-- Assign `False' to pebble_positioning_enabled.
			-- (from EV_PICK_AND_DROPABLE_I)

	disable_transport
			-- Deactivate pick/drag and drop mechanism.
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			is_transport_disabled: not is_transport_enabled

	disable_user_resize
			-- Forbid the resize of the window.

	enable_border
			-- Ensure a border is displayed around `Current'
			-- and set internal_is_border_enabled to `True'.
		ensure
			is_border_enabled: is_border_enabled

	enable_dockable
			-- Allow `Current' to be dockable
			-- (from EV_DOCKABLE_SOURCE_I)
		ensure -- from EV_DOCKABLE_SOURCE_I
			is_dockable: is_dockable

	enable_docking
			-- Ensure is_docking_enabled is True.
			-- `Current' will accept docking from a
			-- compatible EV_DOCKABLE_SOURCE.
			-- (from EV_DOCKABLE_TARGET_I)
		ensure -- from EV_DOCKABLE_TARGET_I
			is_dockable: is_docking_enabled
			id_stored_in_application: (create {EV_ENVIRONMENT}).application.implementation.dockable_targets.has (interface.object_id)

	enable_external_docking
			-- Allow `Current' to be docked into an EV_DOCKABLE_DIALOG
			-- When there is no valid EV_DRAGABLE_TARGET upon completion
			-- of the transport?
			-- (from EV_DOCKABLE_SOURCE_I)
		require -- from EV_DOCKABLE_SOURCE_I
			is_dockable: is_dockable
		ensure -- from EV_DOCKABLE_SOURCE_I
			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_I)
		require -- from EV_DOCKABLE_SOURCE_I
			external_docking_enabled: is_external_docking_enabled
		ensure -- from EV_DOCKABLE_SOURCE_I
			external_docking_not_relative: is_external_docking_relative

	enable_pebble_positioning
			-- Assign `True' to pebble_positioning_enabled.
			-- (from EV_PICK_AND_DROPABLE_I)

	enable_transport
			-- Activate pick/drag and drop mechanism.
			-- (from EV_PICK_AND_DROPABLE_I)
		require -- from EV_PICK_AND_DROPABLE_I
			pebble_not_void: pebble /= Void or pebble_function /= Void
		ensure -- from EV_PICK_AND_DROPABLE_I
			is_transport_enabled: interface.implementation.is_transport_enabled

	enable_user_resize
			-- Allow the resize of the window.

	forbid_resize
			-- Forbid the resize of the window.

	hide
			-- Request that `Current' not be displayed when its parent is.
			-- (from EV_WIDGET_I)

	internal_disable_dockable
			-- Platform specific implementation of disable_dockable.
			-- (from EV_DOCKABLE_SOURCE_I)

	internal_enable_dockable
			-- Platform specific implementation of enable_dockable.
			-- (from EV_DOCKABLE_SOURCE_I)

	lock_update
			-- Lock updates for this window on certain platforms until
			-- unlock_update is called.

	merge_radio_button_groups (other: EV_CONTAINER)
			-- Merge `Current' radio button group with that of `other'.
			-- (from EV_CONTAINER_I)

	remove_default_key_processing_handler
			-- Ensure default_key_processing_handler is Void.
			-- (from EV_WIDGET_I)
		ensure -- from EV_WIDGET_I
			default_key_processing_handler_removed: default_key_processing_handler = Void

	remove_menu_bar
			-- Set menu_bar to `Void'.
		ensure
			menu_bar_void: menu_bar = Void

	remove_pebble
			-- Remove pebble.
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			pebble_removed: pebble = Void and pebble_function = Void
			is_transport_disabled: not is_transport_enabled

	remove_real_source
			-- Ensure real_source is `Void'.
			-- (from EV_DOCKABLE_SOURCE_I)
		require -- from EV_DOCKABLE_SOURCE_I
			is_dockable: is_dockable
		ensure -- from EV_DOCKABLE_SOURCE_I
			real_source_void: real_source = Void

	remove_real_target
			-- Ensure real_target is `Void'.
			-- (from EV_WIDGET_I)
		ensure -- from EV_WIDGET_I
			real_target_void: real_target = Void

	reset_pebble_function
			-- Reset any values created by calling pebble_function.
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			pebble_function_preserved: pebble_function = old pebble_function
			pebble_without_function: pebble_function = Void implies (pebble = old pebble)
			pebble_with_function: pebble_function /= Void implies pebble = 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_I)

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

	set_configurable_target_menu_handler (a_handler: like configurable_target_menu_handler)
			-- Set Configurable Target Menu Handler to `a_handler'.
			-- (from EV_PICK_AND_DROPABLE_I)

	set_configurable_target_menu_mode
			-- Set transport mechanism to a configurable target_menu.
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			mode_is_target_menu: mode_is_configurable_target_menu

	set_default_colors
			-- Set foreground and background color to their default values.
			-- (from EV_COLORIZABLE_I)

	set_default_key_processing_handler (a_handler: like default_key_processing_handler)
			-- Assign default_key_processing_handler to `a_handler'.
			-- (from EV_WIDGET_I)

	set_deny_cursor (a_cursor: like deny_cursor)
			-- Set `a_cursor' to be displayed when the screen pointer is over a
			-- target that doesn't accept pebble during pick and drop.
			-- (from EV_PICK_AND_DROPABLE_I)

	set_drag_and_drop_mode
			-- Set transport mechanism to drag and drop,
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			mode_is_drag_and_drop: mode_is_drag_and_drop

	set_focus
			-- Grab keyboard focus.
			-- (from EV_WIDGET_I)

	set_height (a_height: INTEGER_32)
			-- Set the vertical size to `a_height'.
			-- (from EV_POSITIONABLE_I)
		require -- from EV_POSITIONABLE_I
			a_height_positive_or_zero: a_height >= 0
		ensure -- from EV_POSITIONABLE_I
			height_assigned: height = minimum_height or else height = a_height

	set_maximum_height (value: INTEGER_32)
			-- Make `value' the new maximum_height.
		require
			large_enough: value >= 0
		ensure
			maximum_height_set: maximum_height = value

	set_maximum_size (mw, mh: INTEGER_32)
			-- Make `mw' the new minimum_width and `mh' the new
			-- minimum_height.
		require
			valid_width: mw >= minimum_width
			valid_height: mh >= minimum_height

	set_maximum_width (value: INTEGER_32)
			-- Make `value' the new maximum_width.
		require
			large_enough: value >= 0
		ensure
			maximum_width_set: maximum_width = value

	set_menu_bar (a_menu_bar: EV_MENU_BAR)
			-- Set menu_bar to `a_menu_bar'.
		require
			no_menu_bar_assigned: menu_bar = Void
			a_menu_bar_not_void: a_menu_bar /= Void
		ensure
			assigned: menu_bar = a_menu_bar

	set_pebble (a_pebble: like pebble)
			-- Assign `a_pebble' to pebble.
			-- (from EV_PICK_AND_DROPABLE_I)
		require -- from EV_PICK_AND_DROPABLE_I
			a_pebble_not_void: a_pebble /= Void
		ensure -- from EV_PICK_AND_DROPABLE_I
			pebble_assigned: interface.implementation.pebble = a_pebble
			is_transport_enabled: interface.implementation.is_transport_enabled

	set_pebble_function (a_function: FUNCTION [ANY, TUPLE, ANY])
			-- Assign `a_function' to pebble_function.
			-- (from EV_PICK_AND_DROPABLE_I)
		require -- from EV_PICK_AND_DROPABLE_I
			a_function_not_void: a_function /= Void
		ensure -- from EV_PICK_AND_DROPABLE_I
			pebble_function_assigned: interface.implementation.pebble_function = a_function
			is_transport_enabled: interface.implementation.is_transport_enabled

	set_pebble_position (a_x, a_y: INTEGER_32)
			-- Set the initial position for pick and drop relative to `Current'.
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			pick_x_assigned: pick_x = a_x
			pick_y_assigned: pick_y = a_y

	set_pick_and_drop_mode
			-- Set transport mechanism to pick and drop,
			-- (from EV_PICK_AND_DROPABLE_I)
		ensure -- from EV_PICK_AND_DROPABLE_I
			mode_is_pick_and_drop: mode_is_pick_and_drop