DV_BOX Flat contracts

indexing
description: "Box container for display elements"
date: "$Date$"
revision: "$Revision$"

deferred class interface
DV_BOX

feature -- Initialization

make
-- Initialize.

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

set_default
-- Initialize default values

feature -- Initialization

frozen default_create
-- Standard creation procedure.
-- (from EV_ANY)
ensure then -- from EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state

feature -- Access

accept_cursor: EV_CURSOR
-- Result is cursor displayed when the screen pointer is over a
-- target that accepts pebble during pick and drop.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor

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

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

cursor: EV_DYNAMIC_LIST_CURSOR [EV_WIDGET]
-- Current cursor position.
-- (from EV_DYNAMIC_LIST)
ensure then -- from EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.cursor)

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

deny_cursor: EV_CURSOR
-- 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)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor

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

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

has (v: like item): BOOLEAN
-- Does chain include v?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
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 recursivly 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

i_th (i: INTEGER): EV_WIDGET
-- Item at i-th position.
-- (from EV_DYNAMIC_LIST)
require -- from TABLE
valid_key: valid_index (k)
ensure then -- from EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.i_th (i))

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

index: INTEGER
-- Current position.
-- (from EV_DYNAMIC_LIST)
ensure then -- from EV_DYNAMIC_LIST
bridge_ok: Result = implementation.index

index_of (v: like item; i: INTEGER): INTEGER
-- Index of ith occurence 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_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
-- Is a_widget parent, or recursivly, parent of parent.
-- (from EV_WIDGET)
require -- from EV_DYNAMIC_LIST
a_list_not_void: a_list /= void
require -- from EV_WIDGET
not_destroyed: not is_destroyed

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

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

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

sequential_occurrences (v: EV_WIDGET): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
ensure -- from BAG
non_negative_occurrences: Result >= 0

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

pebble: ANY
-- Data to be transported by pick and drop mechanism.
-- (from EV_PICK_AND_DROPABLE)
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)
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
-- Initial x position for pick and drop relative to Current.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position

pebble_y_position: INTEGER
-- Initial y position for pick and drop relative to Current.
-- (from EV_PICK_AND_DROPABLE)
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_CURSOR
-- Cursor displayed when pointer is over this widget.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed

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

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

feature -- Measurement

client_height: INTEGER
-- 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
-- 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
-- Number of items.
-- (from EV_DYNAMIC_LIST)
ensure then -- from EV_DYNAMIC_LIST
bridge_ok: Result = implementation.count

height: INTEGER
-- 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

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

minimum_height: INTEGER
-- 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
-- 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
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
ensure -- from BAG
non_negative_occurrences: Result >= 0

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

screen_x: INTEGER
-- 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
-- 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

width: INTEGER
-- 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
-- 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
-- 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

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

feature -- Status report

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

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

border_width: INTEGER
-- 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

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

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

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

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

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

is_default_non_expand: BOOLEAN
-- Can't elements be expanded by default?

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_empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)

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

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

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

padding: INTEGER
-- Space between children in pixels.
-- (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_CHAIN)

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

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)
ensure then -- from EV_DYNAMIC_LIST
bridge_ok: Result = implementation.valid_cursor (p)

valid_cursor_index (i: INTEGER): 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): BOOLEAN
-- Is i within allowable bounds?
-- (from CHAIN)
ensure then -- from INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
ensure then -- from CHAIN
valid_index_definition: Result = ((i >= 1) and (i <= count))

writable: BOOLEAN
-- Is there a current item that may be modified?
-- (from SEQUENCE)
require -- from ACTIVE
True
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_borders
-- Display without borders.

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.
ensure
is_default_non_expand: is_default_non_expand

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 avalible 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.

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.

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.
ensure
is_default_expand: not is_default_non_expand

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 avalible 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.

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.
-- Make is_show_requested False.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
not_is_show_requested: not is_show_requested

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

set_accept_cursor (a_cursor: EV_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: 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_border_width (value: INTEGER)
-- 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_default_colors
-- Set foreground and background color to their default values.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed

set_deny_cursor (a_cursor: EV_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: 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
ensure -- from EV_WIDGET
has_focus: has_focus

set_padding (value: INTEGER)
-- Assign value to 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: 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)
-- 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_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)
-- Assign a_name to target_name.
-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
require -- from EV_ABSTRACT_PICK_AND_DROPABLE
a_name_not_void: a_name /= void
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
target_name_assigned: a_name /= target_name and a_name.is_equal (target_name)

show
-- Request that Current be displayed when its parent is.
-- True by default.
-- Make is_show_requested True.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
is_show_requested: is_show_requested

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)
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)
-- 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)
-- Move cursor i positions.
-- (from EV_DYNAMIC_LIST)
ensure -- from CHAIN
too_far_right: (old index + i > count) implies exhausted
too_far_left: (old index + i < 1) implies exhausted
expected_index: (not exhausted) implies (index = old index + i)

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

start
-- Move cursor to first position.
-- (from EV_DYNAMIC_LIST)
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 [EV_WIDGET])
-- Append a copy of s.
-- (from SEQUENCE)
require -- from SEQUENCE
argument_not_void: s /= void
ensure -- from SEQUENCE
new_count: count >= old count

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

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

merge_left (other: like Current)
-- Merge other into current structure before cursor
-- position. Do not move cursor. Empty other.
-- (from EV_DYNAMIC_LIST)
require -- from DYNAMIC_CHAIN
extendible: extendible
not_before: not before
other_exists: other /= void
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
ensure then -- from DYNAMIC_LIST
other_empty: other.is_empty

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

put (v: like item)
-- Replace current item by v.
-- (Synonym for replace)
-- (from CHAIN)
require -- from COLLECTION
extendible: extendible
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_not_window: not v.conforms_to (create {EV_WINDOW})
ensure -- from COLLECTION
item_inserted: is_inserted (v)
ensure then -- from SET
in_set_already: old has (v) implies (count = old count)
added_to_set: not old has (v) implies (count = old count + 1)
ensure then -- from CHAIN
same_count: count = old count
ensure -- from EV_CONTAINER
has_v: has (v)

put (v: like item)
-- Replace current item by v.
-- (Synonym for replace)
-- (from CHAIN)
require -- from COLLECTION
extendible: extendible
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_not_window: not v.conforms_to (create {EV_WINDOW})
ensure -- from COLLECTION
item_inserted: is_inserted (v)
ensure then -- from SET
in_set_already: old has (v) implies (count = old count)
added_to_set: not old has (v) implies (count = old count + 1)
ensure then -- from CHAIN
same_count: count = old count
ensure -- from EV_CONTAINER
has_v: has (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)
-- 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

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_not_window: not v.conforms_to (create {EV_WINDOW})
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)
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 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
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)
-- Set a_minimum_height in pixels to minimum_height.
-- If height is less than a_minimim_height, resize.
-- This setting takes effect next time application is idle.
-- 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

set_minimum_size (a_minimum_width, a_minimum_height: INTEGER)
-- 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.
-- This setting takes effect next time application is idle.
-- 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

set_minimum_width (a_minimum_width: INTEGER)
-- Assign a_minimum_width in pixels to minimum_width.
-- If width is less than a_minimim_width, resize.
-- This setting takes effect next time application is idle.
-- 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

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)

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

feature -- Removal

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

dl_prune (v: like item)
-- Remove first occurrence of v, if any,
-- after cursor position.
-- If found, move cursor to right neighbor;
-- if not, make structure exhausted.
-- (from DYNAMIC_CHAIN)
require -- from COLLECTION
prunable: prunable

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
ensure -- from COLLECTION
no_more_occurrences: not has (v)
ensure then -- from DYNAMIC_CHAIN
is_exhausted: exhausted

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

remove_left
-- Remove item to left of cursor position.
-- Do not move cursor.
-- (from EV_DYNAMIC_LIST)
require -- from DYNAMIC_CHAIN
left_exists: index > 1
require else -- from DYNAMIC_LIST
not_before: not before
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
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)

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)

feature -- Basic operations

extend (widget: EV_WIDGET)
-- Add widget to end of structure.
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_not_window: not v.conforms_to (create {EV_WINDOW})
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_CONTAINER
has_v: has (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)

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

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

propagate_background_color
-- Propagate background_color 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 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

set_default_border_width (new_border_width: INTEGER)
-- Set new_border_width as default border width.

set_default_padding (new_padding: INTEGER)
-- Set new_padding as default padding.

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

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

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)
ensure -- from EV_PICK_AND_DROPABLE_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)
ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void

focus_in_actions: EV_FOCUS_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_FOCUS_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

new_item_actions: EV_NEW_ITEM_ACTION_SEQUENCE
-- Actions to be performed when a new item is added.
-- (from EV_CONTAINER_ACTION_SEQUENCES)
ensure -- from EV_CONTAINER_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)
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)
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 [ANY, TUPLE [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 [ANY, TUPLE [EV_WIDGET]]; test: FUNCTION [ANY, TUPLE [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_exits: test /= void

for_all (test: FUNCTION [ANY, TUPLE [EV_WIDGET], BOOLEAN]): BOOLEAN
-- Is test true for all items?
-- (from LINEAR)
require -- from TRAVERSABLE
test_exits: test /= void

there_exists (test: FUNCTION [ANY, TUPLE [EV_WIDGET], BOOLEAN]): BOOLEAN
-- Is test true for at least one item?
-- (from LINEAR)
require -- from TRAVERSABLE
test_exits: test /= 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 ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
-- 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 EV_COLORIZABLE
background_color_not_void: is_usable implies background_color /= void
foreground_color_not_void: is_usable implies foreground_color /= void
-- from EV_POSITIONED
width_not_negative: is_usable implies width >= 0
height_not_negative: is_usable implies height >= 0
minimum_width_not_negative: is_usable implies minimum_width >= 0
minimum_height_not_negative: is_usable implies minimum_height >= 0
-- from LIST
before_definition: before = (index = 0)
after_definition: after = (index = count + 1)
-- from CHAIN
non_negative_index: index >= 0
index_small_enough: index <= count + 1
off_definition: off = ((index = 0) or (index = count + 1))
isfirst_definition: isfirst = ((not is_empty) and (index = 1))
islast_definition: islast = ((not is_empty) and (index = count))
item_corresponds_to_index: (not off) implies (item = i_th (index))
index_set_has_same_count: index_set.count = count
-- from ACTIVE
writable_constraint: writable implies readable
empty_constraint: is_empty implies (not readable) and (not writable)
-- from INDEXABLE
index_set_not_void: index_set /= void
-- from BILINEAR
not_both: not (after and before)
before_constraint: before implies off
-- from LINEAR
after_constraint: after implies off
-- from TRAVERSABLE
empty_constraint: is_empty implies off
-- from FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
-- from DYNAMIC_CHAIN
extendible: extendible

indexing
library: "[
EiffelStore: library of reusable components for ISE Eiffel.
]"
status: "[
Copyright (C) 1986-2001 Interactive Software Engineering Inc.
All rights reserved. Duplication and distribution prohibited.
May be used only with ISE Eiffel, under terms of user license.
Contact ISE for any other use.
]"
source: "[
Interactive Software Engineering Inc.
ISE Building
360 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Electronic mail <info@eiffel.com>
Customer support http://support.eiffel.com
]"
info: "[
For latest info see award-winning pages: http://eiffel.com
]"

end -- class DV_BOX