-- Automatic generation produced by ISE Eiffel --
indexing
description:
"EiffelVision table. Invisible container that allows %
% unlimited number of other widgets to be packed inside it.%
% A table controls the children's location and size%
% automatically."
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
EV_TABLE
create
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
make_for_test
-- Create with action for testing purposes.
feature -- Initialization
make_from_array (a: ARRAY [EV_WIDGET])
-- Initialize from the items of a.
-- (Useful in proper descendants of class ARRAY,
-- to initialize an array-like object from a manifest array.)
-- (from ARRAY)
require -- from ARRAY
array_exists: a /= void
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)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.actual_drop_target_agent
background_color: EV_COLOR
-- Color displayed behind foreground features.
-- (from EV_COLORIZABLE)
ensure -- from EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.background_color)
columns: INTEGER
-- Number of columns in Current.
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
entry (i: INTEGER): EV_WIDGET
-- Entry at index i, if in index interval
-- (from ARRAY)
require -- from ARRAY
valid_key: valid_index (i)
foreground_color: EV_COLOR
-- Color of foreground features like text.
-- (from EV_COLORIZABLE)
ensure -- from EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.foreground_color)
has (v: EV_WIDGET): BOOLEAN
-- Does v appear in array?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from ARRAY)
ensure -- from CONTAINER
not_found_in_empty: Result implies not is_empty
has_recursive (an_item: like container_item): BOOLEAN
-- Does structure include an_item or
-- does any structure recursively included by structure,
-- include an_item.
-- (from EV_CONTAINER)
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)
ensure -- from EV_HELP_CONTEXTABLE
bridge_ok: Result = implementation.help_context
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
is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
-- Is a_widget parent, or recursively, parent of parent.
-- (from EV_WIDGET)
item (a_column, a_row: INTEGER): EV_WIDGET
-- Widget at coordinates (row, column)
require
valid_row: (1 <= a_row) and (a_row <= rows)
valid_column: (1 <= a_column) and (a_column <= columns)
item_list: ARRAYED_LIST [EV_WIDGET]
-- List of items in Current.
frozen
object_id: INTEGER
-- 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)
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)
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_COORDINATES
-- Position of the screen pointer relative to Current.
-- (from EV_WIDGET)
require -- from EV_WIDGET
is_show_requested: is_show_requested
pointer_style: EV_CURSOR
-- Cursor displayed when pointer is over this widget.
-- (from EV_WIDGET)
rows: INTEGER
-- Number of rows in Current.
target_name: STRING
-- Optional textual name describing Current pick and drop hole.
-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
frozen infix "@" (i: INTEGER): EV_WIDGET
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item.
-- (from ARRAY)
require -- from TABLE
valid_key: valid_index (k)
feature -- Access
area: SPECIAL [EV_WIDGET]
-- Special data zone
-- (from TO_SPECIAL)
feature -- Measurement
additional_space: INTEGER
-- Proposed number of additional items
-- (from RESIZABLE)
ensure -- from RESIZABLE
at_least_one: Result >= 1
capacity: INTEGER
-- Number of available indices
-- Was declared in ARRAY as synonym of count.
-- (from ARRAY)
ensure then -- from ARRAY
consistent_with_bounds: Result = upper - lower + 1
client_height: INTEGER
-- Height of the area available to children in pixels.
-- (from EV_CONTAINER)
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)
ensure -- from EV_CONTAINER
bridge_ok: Result = implementation.client_width
count: INTEGER
-- Number of available indices
-- Was declared in ARRAY as synonym of capacity.
-- (from ARRAY)
ensure then -- from ARRAY
consistent_with_bounds: Result = upper - lower + 1
Growth_percentage: INTEGER is 50
-- Percentage by which structure will grow automatically
-- (from RESIZABLE)
height: INTEGER
-- Vertical size in pixels.
-- Same as minimum_height when not displayed.
-- (from EV_POSITIONED)
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.height
index_set: INTEGER_INTERVAL
-- Range of acceptable indexes
-- (from ARRAY)
ensure -- from INDEXABLE
not_void: Result /= void
ensure then -- from ARRAY
same_count: Result.count = count
same_bounds: ((Result.lower = lower) and (Result.upper = upper))
lower: INTEGER
-- Minimum index
-- (from ARRAY)
Minimal_increase: INTEGER is 5
-- Minimal number of additional items
-- (from RESIZABLE)
minimum_height: INTEGER
-- Lower bound on height in pixels.
-- (from EV_POSITIONED)
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)
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.minimum_width
positive_or_zero: Result >= 0
occurrences (v: EV_WIDGET): INTEGER
-- Number of times v appears in structure
-- (from ARRAY)
ensure -- from BAG
non_negative_occurrences: Result >= 0
screen_x: INTEGER
-- Horizontal offset relative to left of screen in pixels.
-- (from EV_WIDGET)
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)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.screen_y
upper: INTEGER
-- Maximum index
-- (from ARRAY)
width: INTEGER
-- Horizontal size in pixels.
-- Same as minimum_width when not displayed.
-- (from EV_POSITIONED)
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.width
x_position: INTEGER
-- Horizontal offset relative to parent x_position in pixels.
-- (from EV_POSITIONED)
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)
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.y_position
feature -- Status report
all_default: BOOLEAN
-- Are all items set to default values?
-- (from ARRAY)
ensure -- from ARRAY
definition: Result = (count = 0 or else ((array_item (upper) = void or else array_item (upper) = array_item (upper).default) and subarray (lower, upper - 1).all_default))
area_clear (a_column, a_row, column_span, row_span: INTEGER): BOOLEAN
-- Are the cells represented by parameters free of widgets?
require
table_wide_enough: a_column + (column_span - 1) <= columns
table_tall_enough: a_row + (row_span - 1) <= rows
border_width: INTEGER
-- Spacing between edge of Current and outside edge items,
-- in pixels.
column_clear (a_column: INTEGER): BOOLEAN
-- Is column a_column free of widgets?
require
a_column_positive: a_column >= 1
a_column_in_table: a_column <= columns
column_spacing: INTEGER
-- Spacing between two consecutive columns, in pixels.
columns_resizable_to (a_column: INTEGER): BOOLEAN
-- May the column count be resized to a_column?
require
a_column_positive: a_column >= 1
extendible: BOOLEAN
-- May items be added?
-- (Answer: no, although array may be resized.)
-- (from ARRAY)
full: BOOLEAN
-- Is structure filled to capacity? (Answer: yes)
-- (from ARRAY)
has_capture: BOOLEAN
-- Does widget have capture?
-- (from EV_WIDGET)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.has_capture
has_focus: BOOLEAN
-- Does widget have the keyboard focus?
-- (from EV_WIDGET)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.has_focus
frozen id_freed: BOOLEAN
-- Has Current been removed from the table?
-- (from IDENTIFIED)
is_displayed: BOOLEAN
-- Is Current visible on the screen?
-- True when show requested and parent displayed.
-- (from EV_WIDGET)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.is_displayed
is_empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
is_sensitive: BOOLEAN
-- Is object sensitive to user input.
-- (from EV_SENSITIVE)
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)
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.is_show_requested
mode_is_drag_and_drop: BOOLEAN
-- Is the user interface mode drag and drop?
-- (from EV_PICK_AND_DROPABLE)
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)
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)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_target_menu
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
prunable: BOOLEAN
-- May items be removed? (Answer: no.)
-- (from ARRAY)
Readable: BOOLEAN is True
-- Current is always readable.
resizable: BOOLEAN
-- May capacity be changed? (Answer: yes.)
-- (from RESIZABLE)
row_clear (a_row: INTEGER): BOOLEAN
-- Is row a_row free of widgets?
require
a_row_positive: a_row >= 1
a_row_in_table: a_row <= rows
row_spacing: INTEGER
-- Spacing between two consecutive rows, in pixels.
rows_resizable_to (a_row: INTEGER): BOOLEAN
-- May the row count be resized to a_row?
require
a_row_positive: a_row >= 1
same_items (other: like Current): BOOLEAN
-- Do other and Current have same items?
-- (from ARRAY)
require -- from ARRAY
other_not_void: other /= void
ensure -- from ARRAY
definition: Result = ((count = other.count) and then (count = 0 or else (array_item (upper) = other.array_item (other.upper) and subarray (lower, upper - 1).same_items (other.subarray (other.lower, other.upper - 1)))))
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the array?
-- (from ARRAY)
ensure then -- from INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
valid_index_set: BOOLEAN
-- (from ARRAY)
widget_count: INTEGER
-- Number of widgets in Current.
Writable: BOOLEAN is True
-- Current is always writeable.
feature -- Status setting
center_pointer
-- Position screen pointer over center of Current.
-- (from EV_WIDGET)
compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison
compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison
disable_capture
-- Disable grab of all user input events.
-- (from EV_WIDGET)
ensure -- from EV_WIDGET
not_has_capture: not has_capture
disable_pebble_positioning
-- Assign False to pebble_positioning_enabled.
-- (from EV_PICK_AND_DROPABLE)
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)
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
is_displayed: is_displayed
ensure -- from EV_WIDGET
has_capture: has_capture
enable_pebble_positioning
-- Assign True to pebble_positioning_enabled.
-- (from EV_PICK_AND_DROPABLE)
ensure -- from EV_PICK_AND_DROPABLE
pebble_positioning_updated: pebble_positioning_enabled
enable_sensitive
-- Make object sensitive to user input.
-- (from EV_SENSITIVE)
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)
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
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
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)
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)
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
is_displayed: is_displayed
is_sensitive: is_sensitive
ensure -- from EV_WIDGET
has_focus: has_focus
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.
-- (from EV_PICK_AND_DROPABLE)
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)
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)
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)
ensure -- from EV_WIDGET
is_show_requested: is_show_requested
feature -- Element change
add (v: like item; a_column, a_row, column_span, row_span: INTEGER)
-- Set the position of the widgets in one-based coordinates.
--
-- 1 2
-- +----------+---------+
-- 1 |xxxxxxxxxxxxxxxxxxxx|
-- +----------+---------+
-- 2 | | |
-- +----------+---------+
--
-- To describe the widget in the table as shown above,
-- the corresponding coordinates would be (1, 1, 2, 1)
-- Was declared in EV_TABLE as synonym of put.
require
v_not_void: v /= void
v_not_current: v /= Current
v_not_contained: not has (v)
v_parent_void: v.parent = void
v_not_parent_of_current: not is_parent_recursive (v)
a_column_positive: a_column >= 1
a_row_positive: a_row >= 1
column_span_positive: column_span >= 1
row_span_positive: row_span >= 1
table_wide_enough: a_column + (column_span - 1) <= columns
table_tall_enough: a_row + (row_span - 1) <= rows
table_area_clear: area_clear (a_column, a_row, column_span, row_span)
ensure
item_inserted: has (v)
enter (v: like array_item; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
-- (from ARRAY)
require -- from ARRAY
valid_key: valid_index (i)
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
put (v: like item; a_column, a_row, column_span, row_span: INTEGER)
-- Set the position of the widgets in one-based coordinates.
--
-- 1 2
-- +----------+---------+
-- 1 |xxxxxxxxxxxxxxxxxxxx|
-- +----------+---------+
-- 2 | | |
-- +----------+---------+
--
-- To describe the widget in the table as shown above,
-- the corresponding coordinates would be (1, 1, 2, 1)
-- Was declared in EV_TABLE as synonym of add.
require
v_not_void: v /= void
v_not_current: v /= Current
v_not_contained: not has (v)
v_parent_void: v.parent = void
v_not_parent_of_current: not is_parent_recursive (v)
a_column_positive: a_column >= 1
a_row_positive: a_row >= 1
column_span_positive: column_span >= 1
row_span_positive: row_span >= 1
table_wide_enough: a_column + (column_span - 1) <= columns
table_tall_enough: a_row + (row_span - 1) <= rows
table_area_clear: area_clear (a_column, a_row, column_span, row_span)
ensure
item_inserted: has (v)
remove (v: EV_WIDGET)
-- Remove v from Current if present.
require
item_not_void: v /= void
item_in_table: has (v)
ensure
item_removed: not has (v)
remove_help_context
-- Remove key press action associated with EV_APPLICATION.help_key.
-- (from EV_HELP_CONTEXTABLE)
require -- from EV_HELP_CONTEXTABLE
help_context_not_void: help_context /= void
ensure -- from EV_HELP_CONTEXTABLE
no_help_context: help_context = void
set_background_color (a_color: like background_color)
-- Assign a_color to foreground_color.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
a_color_not_void: a_color /= void
ensure -- from EV_COLORIZABLE
background_color_assigned: background_color.is_equal (a_color)
set_foreground_color (a_color: like foreground_color)
-- Assign a_color to foreground_color.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
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
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
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
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
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
a_cursor_not_void: a_cursor /= void
ensure -- from EV_WIDGET
pointer_style_assigned: pointer_style.is_equal (a_cursor)
subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER)
-- Copy items of other within bounds start_pos and end_pos
-- to current array starting at index index_pos.
-- (from ARRAY)
require -- from ARRAY
other_not_void: other /= void
valid_start_pos: other.valid_index (start_pos)
valid_end_pos: other.valid_index (end_pos)
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
valid_index_pos: valid_index (index_pos)
enough_space: (upper - index_pos) >= (end_pos - start_pos)
feature -- Removal
clear_all
-- Reset all items to default values.
-- (from ARRAY)
ensure -- from ARRAY
stable_lower: lower = old lower
stable_upper: upper = old upper
default_items: all_default
discard_items
-- Reset all items to default values with reallocation.
-- (from ARRAY)
ensure -- from ARRAY
default_items: all_default
frozen free_id
-- Free the entry associated with object_id if any
-- (from IDENTIFIED)
ensure -- from IDENTIFIED
object_freed: id_freed
prune_all (v: EV_WIDGET)
-- Remove all occurrences of v.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from COLLECTION)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
no_more_occurrences: not has (v)
feature -- Resizing
automatic_grow
-- Change the capacity to accommodate at least
-- Growth_percentage more items.
-- (from RESIZABLE)
ensure -- from RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100
grow (i: INTEGER)
-- Change the capacity to at least i.
-- (from ARRAY)
ensure -- from RESIZABLE
new_capacity: capacity >= i
feature -- Conversion
linear_representation: LINEAR [EV_WIDGET]
-- Representation as a linear structure
feature -- Conversion
to_c: ANY
-- Address of actual sequence of values,
-- for passing to external (non-Eiffel) routines.
-- (from ARRAY)
feature -- Duplication
frozen ev_clone: like Current
-- New object that is_equal to Current.
-- To change copying/cloning semantics, redefine copy.
-- (from EV_ANY)
ensure -- from EV_ANY
equal: equal (Result, Current)
subarray (start_pos, end_pos: INTEGER): like Current
-- Array made of items of current array within
-- bounds start_pos and end_pos.
-- (from ARRAY)
require -- from ARRAY
valid_start_pos: valid_index (start_pos)
valid_end_pos: valid_index (end_pos)
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
ensure -- from ARRAY
lower: Result.lower = start_pos
upper: Result.upper = end_pos
feature -- Basic operations
propagate_background_color
-- Propagate background_color to all children.
-- (from EV_CONTAINER)
ensure -- from EV_CONTAINER
background_color_propagated: background_color_propagated
propagate_foreground_color
-- Propagate foreground_color to all children.
-- (from EV_CONTAINER)
ensure -- from EV_CONTAINER
foreground_color_propagated: foreground_color_propagated
feature -- Inapplicable
prune (v: EV_WIDGET)
-- Remove first occurrence of v if any.
-- (Precondition is False.)
-- (from ARRAY)
require -- from COLLECTION
prunable: prunable
feature -- Implementation
Changeable_comparison_criterion: BOOLEAN is False
-- May object_comparison be changed?
-- (Answer: no by default.)
-- (from EV_CONTAINER)
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
all_radio_buttons_connected: BOOLEAN
-- Are all radio buttons in this container connected?
-- (from EV_CONTAINER)
background_color_propagated: BOOLEAN
-- Do all children have same background color as Current?
-- (from EV_CONTAINER)
foreground_color_propagated: BOOLEAN
-- Do all children have same foreground color as Current?
-- (from EV_CONTAINER)
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 key is pressed.
-- (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
proximity_in_actions: EV_PROXIMITY_ACTION_SEQUENCE
-- Actions to be performed when pointing device comes into range.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void
proximity_out_actions: EV_PROXIMITY_ACTION_SEQUENCE
-- Actions to be performed when pointing device goes out of range.
-- (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 -- Status Report
default_create_called: BOOLEAN
-- Has default_create been called?
-- (from EV_ANY)
is_destroyed: BOOLEAN
-- Is Current no longer usable?
-- (from EV_ANY)
ensure -- from EV_ANY
bridge_ok: Result = implementation.is_destroyed
feature -- Status settings
disable_homogeneous
-- Allow items to have varying sizes.
enable_homogeneous
-- Set each item in Currnet to be equal in size
-- to that of the largest item.
resize (a_column, a_row: INTEGER)
-- Resize the table to hold a_column by a_row widgets.
require
a_column_positive: a_column >= 1
a_row_positive: a_row >= 1
columns_resizeable: columns_resizable_to (a_column)
rows_resizeable: rows_resizable_to (a_row)
ensure
columns_set: columns = a_column
rows_set: rows = a_row
upper_updated: upper = rows * columns
items_untouched: item_list.is_equal (old item_list)
set_border_width (a_value: INTEGER)
-- Assign a_value to border_width.
require
positive_value: a_value >= 0
set_column_spacing (a_value: INTEGER)
-- Assign a_value to the spacing in-between columns, in pixels.
require
positive_value: a_value >= 0
set_row_spacing (a_value: INTEGER)
-- Assign a_value to the spacing in-between rows, in pixels.
require
positive_value: a_value >= 0
invariant
-- from ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
-- from EV_CONTAINER
client_width_within_bounds: is_useable implies client_width >= 0 and client_width <= width
client_height_within_bounds: is_useable implies client_height >= 0 and client_height <= height
all_radio_buttons_connected: is_useable implies all_radio_buttons_connected
parent_of_items_is_current: is_useable implies parent_of_items_is_current
items_unique: is_useable implies items_unique
-- from EV_WIDGET
pointer_position_not_void: is_useable and is_show_requested implies pointer_position /= void
is_displayed_implies_show_requested: is_useable and is_displayed implies is_show_requested
parent_contains_current: is_useable and 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_useable implies background_color /= void
foreground_color_not_void: is_useable implies foreground_color /= void
-- from EV_POSITIONED
width_not_negative: is_useable implies width >= 0
height_not_negative: is_useable implies height >= 0
minimum_width_not_negative: is_useable implies minimum_width >= 0
minimum_height_not_negative: is_useable implies minimum_height >= 0
-- from ARRAY
consistent_size: capacity = upper - lower + 1
non_negative_count: count >= 0
index_set_has_same_count: valid_index_set
-- from RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
-- from BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
-- from FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
-- from INDEXABLE
index_set_not_void: index_set /= void
end -- class EV_TABLE
-- Generated by ISE Eiffel --
-- For more details: www.eiffel.com --