indexing
description: "[
Widget which is a combination of an EV_TREE and an EV_MULTI_COLUMN_LIST.
Item Insertion:
The grid is an item holder for objects of type EV_GRID_ITEM and its descendents. Each grid
item may be inserted in to the grid at a specific column and row. An item itself may be
added to the grid via set_item, which takes a column and row index. Items be also added
via the set_item routine of the row (EV_GRID_ROW) and column (EV_GRID_COLUMN) objects
contained within `Current'.
Items inserted may be Void if necessary, this may be useful to blank out any existing items
set.
If a grid contains no items and therefore has no rows or columns, inserting an item will
dynamically resize and automatically create the columns and rows so that it can contain
and display the newly inserted item. New columns and rows may also be added to the grid via
insert_new_column and insert_new_row respectively.
--------------------------------------------------------------------------------
Dynamic Mode:
There may be times where you have very large numbers of items you wish to
display into the grid. Unfortunately, the overhead of building thousands and
thousands of grid items and inserting them can take a considerable amount of
which shows up as a delay to users of the system. To prevent this, the grid
supports the use of a dynamic mode which permit you to specify how many items
are contained and then as and when the grid requires access to one of these items
for display purposes, an event is triggered requesting the item to be displayed.
dynamic content is enabled via enable_partial_dynamic_content. In this mode
whenever the grid attempts to draw an item that is `Void', it queries you for the
item and then inserts it into the grid.
The grid requests an item in the dynamic mode through the calling of the
dynamic_content_function which may be set via a call to
set_dynamic_content_function. This function has two integer arguments
corresponding to the column and row index of the desired item and a return type
of EV_GRID_ITEM.
--------------------------------------------------------------------------------
Size and Position:
The grid is comprised of the following graphical elements:
1. A header displayed at the top of `Current' which may be hidden/shown via
show_header and hide_header'.
2. A viewable area in which the contents of `Current' are displayed, displayed
immediately below the header. The size of this
area is given by viewable_width and viewable_height with its position
relative to the top left corner of `Current' given by viewable_x_offset,
viewable_y_offset. Note that viewable_y_offset changes based on the visible
state of the header.
3. A horizontal scroll bar displayed below the viewable area, only shown if the
virtual width of `Current' is greater than viewable_width.
4. A vertical scroll bar displayed to the right of viewable area and header,
only shown if the virtual height of `Current' is greater than viewable_height.
You may supress the displaying of the scroll bars if required via calls to
hide_vertical_scroll_bar and hide_horizontal_scroll_bar which ensure that
the scroll bars are never displayed. This is useful for situations where you
wish to control the virtual position of the grid via your own custom interface.
The virtual size of the grid represents the complete screen area in pixels
required to display the contents of `Current' and may be queried via
virtual_width and virtual_height. If the contents of the grid are smaller
than the viewable area, then the virtual size is equal to the viewable area,
otherwise an area of the virtual size is displayed within viewable area, with
the coordinates of this area (relative to the top left corner) within the
virtual size given by `virtual_x' and `virtual_y'. As the scroll bars are moved,
`virtual_x' and `virtual_y' are directly manipulated, although you may set the
virtual position explicitly via calls to `set_virtual_x' and `set_virtual_y'.
The maximum permitted virtual position of the grid is given by
maximum_virtual_x_position, maximum_virtual_y_position which is dependent on
the following factors:
The viewable area of the grid.
The virtual_width and virtual_height.
The `is_*_scrolling_per_item' properties.
The `is_*_overscroll_enabled' properties.
Changing one or more of these properties may immediately change the virtual width,
height or maximum virtual positions, and possibly scroll the grid to ensure that the
current virtual position is within the new bounds.
The properties is_vertical_overscroll_enabled and is_horizontal_overscroll_enabled
permit you to ensure the grid permits scrolling past the final item, ensuring that there
is trailing space matching the viewable dimension of the grid less the dimension of
the final item.
You may query the virtual position of an item within the virtual area of
`Current' via virtual_x_position and virtual_y_position directly on the
item. You may also query the dimensions of an item via width and height. It
is important to note that for an item that is part of a tree structure, the
width may not be equal to `column.width' and the virtual_x_position may not
be equal to `column.virtual_x_position'. This is because items in tree
structures are indented to provide space for the expand/collapse icons as
necessary. The number of pixels that the item is indented for this purpose may
be queried directly from the item via a call
to `horizontal_indent'.
You may query the virtual y position of a row within `Current' via
virtual_y_position directly on the row.
You may query the virtual x position of a column within `Current' via
virtual_x_position directly on the column.
As items, columns or rows are added and removed from `Current', the virtual size
may change. The virtual position may only change if in this situation, you are
removing rows or columns that cause the virtual size to reduce and the virtual
position is no longer valid. The grid will automatically adjust the virtua
position so that the contents of the viewable area are completely contained
within the new virtual position.
The height of the rows displayed in `Current' is dependent on
is_row_height_fixed. If `True', then all rows are displayed at the same
height, goverened by row_height. If `False', then the height of the row is
goverened by its height property which may differ on an individual row basis.
The width of columns is always unique and based on their width property.
To determine if a particular item is located at a virtual position, use
item_at_virtual_position. You may determine the first and last visible rows
via first_visible_row and last_visible_row, while first_visible_column and
last_visible_column give the first and last columns visible in `Current'. For
more precise information regarding exactly which rows and columns are displayed,
you may query visible_row_indexes and visible_column_indexes. Note that if a
tree is enabled via enable_tree, then the contents of visible_row_indexes
and visible_column_indexes may not be contiguous.
To optimize performance, `Current' only performs recomputation of the virtual
positions of items as strictly necessary, which is normally once just before a
redraw. As you may query virtual position information whenever you wish,
`Current' may be forced to perform its recomputation of virtual positions as a
result of your query. Each time that you modify something in the grid that may
affect a virtual position of an item, the grid must recompute the virtual
positions again as required. Therefore, for your code to be optimal, it may be
necessary to take this into account. The worst possible case scenario is if you
are to iterate from the start of the grid to the end of the grid and modify the
state of each item or row during the iteration before querying a virtual position
of an object in the grid past the current iteration position. In this situation,
it is recommended that you perform a two-pass operation. First perform all of the
modifications to the items and then perform all of the queries to virtual
positions. The grid is optimized for additions in order so if you are repeatedly
adding items and querying their virtual positions, then the performance is far
better than if you are continuously inserting items at the start of the grid and
querying their virtual positions. Although it is important to be aware of this
behavior, you will find that in almost all cases, you have do perform no special
optimizations to get good performance within `Current'. This also aplies to
removal of rows. If you have many rows to remove, start with the final rows and
iterate towards the first for increased performance.
The re-drawing of `Current' is performed on idle, so if you are performing heavy
computation and the grid is not updating, call `process_events' from
EV_APPLICATION in order to force a re-draw.
--------------------------------------------------------------------------------
Appearance:
Each of the items contained within the grid are sized based on the column and
row that they occupy. If is_row_height_fixed is `True' then the height of the
rows is dependent on row_height of `Current', otherwise it is dependent on
height of the row and each row may occupy a different height. For the first
non-`Void' item of each row, the position of the item is `item.horizontal_indent'
pixels greater than the column in which it is contained. The appearance of each
item is dependent on the actual type of the item, but there are a number of
ways in which you may modify this at the grid level.
`post_draw_overlay_function' is available, which permits you to draw directly on
top of items immediately after they are dwan by the implementation. This is
useful for adding custom borders to your items.
`pre_draw_overlay_function' is available, which permits you to draw on top of the
background of items, but before any features of that item have been drawn. For
example, for grid label items, the background is cleared, then the function is
called and then the `text' and `pixmap' are drawn. Note that for drawable items,
which do not re-draw their background automatically, nothing is drawn before the
`pre_draw_overlay_function' is called.
When items are selected in a focused grid, they become highlighted in
focused_selection_color and if the grid does not have the focus,
non_focused_selection_color is used instead. It is recommended that you use
these colors for your own drawable items to maintain consistency within the grid.
The selection colors may be modified via set_focused_selection_color and
set_non_focused_selection_color.
Seperators between items may be enabled on the grid via enable_column_separators
and enable_row_separators which ensure a single line is drawn between each row
and column in separator_color. Use set_separator_color to modify this color.
The tree structure of `Current' is drawn using expand_node_pixmap and
collapse_node_pixmap to illustrate the expanded state of rows with subrows. You
may use your own pixmaps by calling `set_expand_node_pixmap' and
`set_collapse_node_pixmap'. The indent applied to each subrow is based on the
current width of the node pixmaps + subrow_indent. You may increase this indent
by calling set_subrow_indent. The nodes in the tree are connected via lines drawn
in the color tree_node_connector_color which may be modified via
set_tree_node_connector_color. These connecting lines may also be hidden via a
call to hide_tree_node_connectors.
During a column resize in `Current', the contents of the grid are immediately
refreshed. This behavior may be disabled via a call to `disable_column_resize_immedite'
and may be necessary if running the grid on older systems as it is less processor
intensive. When not is_column_resize_immediate, the column resizing is only performed
when the user completes the resize, but a divider may be shown in `Current' which indicates
its new width during the resizing, by calling enable_resizing_divider. This divider
may be solid or dashed, based on the state of is_resizing_divider_solid, settable via
`enable_resizing_divider_solid' or `disable_resizing_divider_solid'.
If you wish to perform multiple updates to the grid, in most cases the graphical
update is buffered until the system becomes idle, thereby reducing flicker.
However, in some situations, it is possible that the system may become idle
during the updates, which may lead to flicker. In situations such as these, you
may use lock_update to prevent graphical updates from occuring in the grid
until unlock_update is called. While the grid is_locked, no graphical updates
of any form are performed.
--------------------------------------------------------------------------------
Selection:
The grid allows both single and multiple selection handling on an item or row level.
When enable_single_item_selection is called, only an single item may be selected by the
user when `Current' is on-screen. Selection may occur either programmatically via the
`enable_select' routine of either the item/column or row or on-screen via mouse or keyboard.
This is accompanied with the query `is_selected'. When a user attempts to select an item or
row on-screen the grid attempts to make that item or row more visible to the user so that the
text of the item may be read, this will not occur however if the item is currently activated.
There are two main selection modes, item selection and row selection. In item selection,
single or multiple items may be selected depending on the current selection mode. This can be
set with enable_single_item_selection and enable_multiple_item_selection respectively.
For each type of selection there are events. Examples of such events are item_select_actions,
row_select_actions and column_select_actions, these are fired in `Current', with the
appropriate object being passed to the action sequence that is selected. item_select_actions
will only get executed whilst in either single or multiple item selection mode. For handling selection
events during single or multiple row selection modes, row_select_actions should be used.
To keep track of deselected items, rows or columns, there is item_deselect_actions,
row_deselect_actions and column_deselect_actions respectively.
Along with selecting items, they may also be deselected. This can be done programatically
via the `disable_select' routine of either the item/column or row.
To query what objects are selected, the following queries are available in `Current',
selected_items, selected_rows and selected_columns.
To turn off any default behavior the following queries are available, disable_selection_key_handling
and `disable_selection_click_handling', this turns off the ability for the user of the grid
to select items via the keyboard or mouse.
The routine enable_always_selected makes sure that at least one item or row is selected depending
on the mode after the initial selection. This can be handy for implementing widgets that require an item
be selected at all times.
The selection of the grid may be removed with remove_selection.
--------------------------------------------------------------------------------
Item Activation:
Activation allows for interactive editing of the contents of an item. By calling
`activate' on an activatable item in response to a user event such as double clicking,
the item allows for in-place user editing, for changing things such as text. After
changing the item, the user may complete the activation by pressing Enter on the
keyboard or by causing the item itself to loose focus.
To programmatically cancel any activation, each grid item has a `deactivate' routine
that may be called during the activation.
If an activation occurs during a user selection then the grid itself will not attempt to reposition
the item so that it is more visible.
When an item is activated, the item_activate_actions are fired, this can be used
to customize the activation process of a certain item, item_deactivate_actions are
fired when the item is deactivated. When an item is deactivated, if the user hasn't
cancelled the deactivation then the item's contents are updated.
See EV_GRID_EDITABLE_ITEM and EV_GRID_COMBO_ITEM for examples of activatable items
that allow for in place editing.
--------------------------------------------------------------------------------
Event Handling:
The standard set of widget events are inherited from EV_CELL with an additional
set of events that are applicable to both `Current' and the items contained are
inherited from EV_GRID_ACTION_SEQUENCES. For example,
pointer_button_press_actions is inherited from EV_CELL, while
pointer_button_press_item_actions is inherited from EV_GRID_ACTION_SEQUENCES
and has an EV_GRID_ITEM as event data specifying the applicable item (if any).
The coordinates of the item specific versions use virtual coordinates of
`Current' as their coordinate information, wheras those inherited from EV_CELL
use client coordinates as for any other EV_WIDGET. The order of event execution
for multiple action sequences that may be triggered by a single event are as
follows:
1. The standard inherited widget events are fired. i.e.
"grid.pointer_button_press_actions" The x and y coordinate event data is
relative to the upper left corner of `Current'.
2. The grid item specific versions of these events are fired. i.e.
"grid.pointer_button_press_item_actions" The x and y coordinate event data is
relative to the upper left corner of the "item" area of `Current', in virtual
grid coordinates. These events are only fired while the mouse pointer is above
the "item" area (does not include header and scroll bars).
3. The events are fired on the item themselves. i.e.
"item.pointer_button_press_actions" The x and y coordinate event data is
relative to the upper left corner of the item.
The grid specific versions of particular events permit you to perform handling
for all of your items in a common place and are always fired before the specific
item versions. For example, if you connect to both EV_GRID.row_expand_actions
and EV_GRID_ROW.expand_actions, the grid version is fired first, immediately by
the row version. The action sequences are fired one immediately after the other
and both are always fired even if you change states of the target object within
the first action sequence.
--------------------------------------------------------------------------------
Color Handling:
Colors applied to items within `Current' are determined on a three level basis.
The base level is `Current' whose foreground_color and background_color may
never be Void.
The second level are the columns and rows of `Current' whose foreground_color
and background_color are `Void' by default.
The final level is comprised of the items of `Current' themselves whose
foreground_color and background_color are `Void' by default.
As `Current' performs a re-draw of an item "cell" contained within, the
following rules are applied in order to determine the displayed colors:
1. If there is an item in the "cell" which has a non-Void foreground_color or
background_color then these colors are applied to the contents of that "cell",
otherwise, step 2 is applied.
2. If the column or row at that position has non-Void foreground_color or
background_color then these colors are applied to the contents of that "cell",
otherwise step 3 is applied.
3. As the colors of the item, row and column were all `Void', the `foreground'
and background_color of `Current' is applied to the contents of that "cell".
Note that for areas of an items "cell" that are not filled by item item itself,
such as the area of a tree structure, step 1 is ignored and the color
calculations begin at step 2.
]"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-08-16 14:19:33 -0700 (Wed, 16 Aug 2006) $"
revision: "$Revision: 62633 $"
class interface
EV_GRID
create
default_create
EV_ANY
require ANY
True
ensure then 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
accept_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor
activated_item: EV_GRID_ITEM
require
not_destroyed: not is_destroyed
actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_ABSTRACT_PICK_AND_DROPABLE]
`Void'`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.actual_drop_target_agent
are_column_separators_enabled: BOOLEAN
separator_color
require
not_destroyed: not is_destroyed
are_row_separators_enabled: BOOLEAN
separator_color
require
not_destroyed: not is_destroyed
are_tree_node_connectors_shown: BOOLEAN
`Current'
require
not_destroyed: not is_destroyed
background_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.background_color)
cell_background_pixmap: EV_PIXMAP
`Result'`Current'
`Current'
EV_CONTAINER
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
bridge_ok: (Result = Void and implementation.background_pixmap = Void) or Result.is_equal (implementation.background_pixmap)
collapse_node_pixmap: EV_PIXMAP
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
column (a_column: INTEGER_32): EV_GRID_COLUMN
`a_column'
require
not_destroyed: not is_destroyed
a_column_positive: a_column > 0
a_column_not_greater_than_column_count: a_column <= column_count
ensure
column_not_void: Result /= Void
column_at_virtual_position (a_virtual_x: INTEGER_32): EV_GRID_COLUMN
`a_virtual_x'
require
not_destroyed: not is_destroyed
virtual_x_valid: a_virtual_x >= 0 and a_virtual_x <= virtual_width
column_deselect_actions: ACTION_SEQUENCE [TUPLE [EV_GRID_COLUMN]]
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
column_select_actions: ACTION_SEQUENCE [TUPLE [EV_GRID_COLUMN]]
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
data: ANY
EV_ANY
default_key_processing_handler: PREDICATE [ANY, TUPLE [EV_KEY]] assign set_default_key_processing_handler
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.default_key_processing_handler
deny_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor
displayed_column (i: INTEGER_32): EV_GRID_COLUMN
`i'
column
hide
require
not_destroyed: not is_destroyed
i_positive: i > 0
i_not_greater_than_displayed_column_count: i <= displayed_column_count
ensure
column_not_void: Result /= Void
dynamic_content_function: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_GRID_ITEM]
is_content_partially_dynamic
require
not_is_destroyed: not is_destroyed
expand_node_pixmap: EV_PIXMAP
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
fill_background_actions: ACTION_SEQUENCE [TUPLE [EV_DRAWABLE, INTEGER_32, INTEGER_32, INTEGER_32, INTEGER_32]]
row_countcolumn_count
background_color
`drawable'width
height
fill_background_actions
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
not_void: Result /= Void
focused_selection_color: EV_COLOR
require
not_is_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
focused_selection_text_color: EV_COLOR
require
not_is_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
foreground_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.foreground_color)
generating_type: STRING_8
ANY
generator: STRING_8
ANY
cell_has (v: EV_WIDGET): BOOLEAN
`Current'`v'
EV_CELL
ensure CONTAINER
not_found_in_empty: Result implies not cell_is_empty
cell_has_recursive (an_item: like cell_item): BOOLEAN
`an_item'
`an_item'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
header: EV_GRID_HEADER
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
help_context: FUNCTION [ANY, TUPLE, EV_HELP_CONTEXT]
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
ensure EV_HELP_CONTEXTABLE
bridge_ok: Result = implementation.help_context
horizontal_scroll_bar: EV_HORIZONTAL_SCROLL_BAR
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
frozen id_object (an_id: INTEGER_32): IDENTIFIED
`an_id'
IDENTIFIED
ensure IDENTIFIED
consistent: Result = Void or else Result.object_id = an_id
is_column_resize_immediate: BOOLEAN
`Current'
`True'is_resizing_divider_enabled
`False'
require
not_destroyed: not is_destroyed
is_content_partially_dynamic: BOOLEAN
`Current'`True'
`Current'
dynamic_content_function
`Current'
require
not_destroyed: not is_destroyed
is_docking_enabled: BOOLEAN
`Current'
`Current'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
bridge_ok: Result = implementation.is_docking_enabled
is_full_redraw_on_virtual_position_change_enabled: BOOLEAN
require
not_is_destroyed: not is_destroyed
is_header_displayed: BOOLEAN
`Current'
require
not_destroyed: not is_destroyed
is_horizontal_overscroll_enabled: BOOLEAN
`Current'
viewable_width
`True'
`False'
require
not_destroyed: not is_destroyed
is_horizontal_scrolling_per_item: BOOLEAN
`True'
`False'
require
not_destroyed: not is_destroyed
is_locked: BOOLEAN
`Current'
unlock_update
require
not_is_destroyed: not is_destroyed
is_resizing_divider_enabled: BOOLEAN
is_column_resize_immediate`True'`Result'
`Current'
require
not_destroyed: not is_destroyed
is_resizing_divider_solid: BOOLEAN
`False'
require
not_destroyed: not is_destroyed
is_row_height_fixed: BOOLEAN
`Current'
require
not_destroyed: not is_destroyed
is_vertical_overscroll_enabled: BOOLEAN
`Current'
viewable_height
`True'
`False'
require
not_destroyed: not is_destroyed
is_vertical_scrolling_per_item: BOOLEAN
`True'
`False'
require
not_destroyed: not is_destroyed
cell_item: EV_WIDGET
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
readable: readable
ensure EV_CONTAINER
bridge_ok: Result = implementation.cell_item
item (a_column: INTEGER_32; a_row: INTEGER_32): EV_GRID_ITEM
`a_row'`a_column'
require
not_destroyed: not is_destroyed
a_column_positive: a_column > 0
a_column_less_than_column_count: a_column <= column_count
a_row_positive: a_row > 0
a_row_less_than_row_count: a_row <= row_count
item_accept_cursor_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], EV_POINTER_STYLE]
item_pebble_function
require
not_destroyed: not is_destroyed
item_activate_actions: ACTION_SEQUENCE [TUPLE [EV_GRID_ITEM, EV_POPUP_WINDOW]]
`activate'{EV_GRID_EDITABLE_ITEM}.activate_action
`popup_window'
`activate_item'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
item_at_virtual_position (a_virtual_x, a_virtual_y: INTEGER_32): EV_GRID_ITEM
`a_virtual_x'`a_virtual_y'
`Void'
require
not_destroyed: not is_destroyed
virtual_x_valid: a_virtual_x >= 0 and a_virtual_x <= virtual_width
virtual_y_valid: a_virtual_y >= 0 and a_virtual_y <= virtual_height
item_deactivate_actions: EV_GRID_ITEM_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
item_deny_cursor_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], EV_POINTER_STYLE]
item_pebble_function
require
not_destroyed: not is_destroyed
item_deselect_actions: EV_GRID_ITEM_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
item_drop_actions: ACTION_SEQUENCE [TUPLE [EV_GRID_ITEM, ANY]]
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
item_pebble_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], ANY]
pebble
require
not_destroyed: not is_destroyed
item_select_actions: EV_GRID_ITEM_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
item_veto_pebble_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM, ANY], BOOLEAN]
require
not_destroyed: not is_destroyed
locked_columns: ARRAYED_LIST [EV_GRID_COLUMN]
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
locked_rows: ARRAYED_LIST [EV_GRID_ROW]
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
maximum_virtual_x_position: INTEGER_32
is_vertical_scrolling_per_item
is_vertical_overscroll_enabled
require
not_destroyed: not is_destroyed
ensure
result_non_negative: Result >= 0
maximum_virtual_y_position: INTEGER_32
is_horizontal_scrolling_per_item
is_horizontal_overscroll_enabled
require
not_destroyed: not is_destroyed
ensure
result_non_negative: Result >= 0
non_focused_selection_color: EV_COLOR
require
not_is_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
non_focused_selection_text_color: EV_COLOR
require
not_is_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
frozen object_id: INTEGER_32
IDENTIFIED
ensure IDENTIFIED
valid_id: id_object (Result) = Current
parent: EV_CONTAINER
`Current'
EV_WIDGET
require EV_CONTAINABLE
not_destroyed: not is_destroyed
ensure then EV_WIDGET
bridge_ok: Result = implementation.parent
pebble: ANY
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble
pebble_function: FUNCTION [ANY, TUPLE, ANY]
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_function
pebble_positioning_enabled: BOOLEAN
`True'
pebble_x_positionpebble_y_position
`False'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_positioning_enabled
pebble_x_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position
pebble_y_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_y_position
pointer_button_press_item_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32, INTEGER_32, EV_GRID_ITEM]]
`Void'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_button_release_item_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32, INTEGER_32, EV_GRID_ITEM]]
`Void'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_double_press_item_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32, INTEGER_32, EV_GRID_ITEM]]
`Void'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_enter_item_actions: ACTION_SEQUENCE [TUPLE [BOOLEAN, EV_GRID_ITEM]]
`on_grid'`True'item
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_leave_item_actions: ACTION_SEQUENCE [TUPLE [BOOLEAN, EV_GRID_ITEM]]
`on_grid'`True'item
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_motion_item_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32, EV_GRID_ITEM]]
`Void'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
pointer_position: EV_COORDINATE
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_show_requested: is_show_requested
pointer_style: EV_POINTER_STYLE
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
post_draw_overlay_actions: ACTION_SEQUENCE [TUPLE [EV_DRAWABLE, EV_GRID_ITEM, INTEGER_32, INTEGER_32]]
`Current'
width`a_column_index'height`a_row_index'
`drawable'
`horizontal_indent'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
not_void: Result /= Void
pre_draw_overlay_actions: ACTION_SEQUENCE [TUPLE [EV_DRAWABLE, EV_GRID_ITEM, INTEGER_32, INTEGER_32]]
`Current'
width`a_column_index'height`a_row_index'
`drawable'
`horizontal_indent'
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
not_void: Result /= Void
real_target: EV_DOCKABLE_TARGET
`Result'
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.real_target
remove_selection
selected_itemsselected_rowsselected_columns
require
not_destroyed: not is_destroyed
ensure
selected_items_empty: selected_items.is_empty
selected_rows_empty: selected_rows.is_empty
selected_columns_empty: selected_columns.is_empty
row (a_row: INTEGER_32): EV_GRID_ROW
`a_row'
require
not_destroyed: not is_destroyed
a_row_positive: a_row > 0
a_row_not_greater_than_row_count: a_row <= row_count
ensure
row_not_void: Result /= Void
row_at_virtual_position (a_virtual_y: INTEGER_32; ignore_locked_rows: BOOLEAN): EV_GRID_ROW
`a_virtual_y'
require
not_destroyed: not is_destroyed
virtual_y_valid: a_virtual_y >= 0 and a_virtual_y <= virtual_height
row_collapse_actions: EV_GRID_ROW_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
row_deselect_actions: EV_GRID_ROW_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
row_expand_actions: EV_GRID_ROW_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
row_height: INTEGER_32
`Current'`Current'
is_row_height_fixed
require
not_destroyed: not is_destroyed
is_row_height_fixed: is_row_height_fixed
ensure
result_non_negative: Result >= 0
row_select_actions: EV_GRID_ROW_ACTION_SEQUENCE
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
selected_columns: ARRAYED_LIST [EV_GRID_COLUMN]
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
selected_items: ARRAYED_LIST [EV_GRID_ITEM]
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
selected_rows: ARRAYED_LIST [EV_GRID_ROW]
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
separator_color: EV_COLOR
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
subrow_indent: INTEGER_32
`parent_row'
require
not_destroyed: not is_destroyed
ensure
result_non_negative: Result >= 0
target_name: STRING_GENERAL
`Current'
EV_ABSTRACT_PICK_AND_DROPABLE
tooltip: STRING_32
`Current'
`Result'
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
bridge_ok: equal (Result, implementation.tooltip)
not_void: Result /= Void
cloned: Result /= implementation.tooltip
vertical_scroll_bar: EV_VERTICAL_SCROLL_BAR
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
veto_dock_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN]
`Result'`True'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
bridge_ok: Result = implementation.veto_dock_function
viewable_height: INTEGER_32
`Current'
require
not_destroyed: not is_destroyed
ensure
viewable_height_valid: viewable_height >= 0 and viewable_height <= height
viewable_width: INTEGER_32
`Current'
require
not_destroyed: not is_destroyed
ensure
viewable_width_valid: viewable_width >= 0 and viewable_width <= width
viewable_x_offset: INTEGER_32
`Current'
viewable_widthviewable_height
require
not_destroyed: not is_destroyed
ensure
viewable_x_offset_valid: Result >= 0 and Result <= width
viewable_y_offset: INTEGER_32
`Current'
viewable_widthviewable_height
require
not_destroyed: not is_destroyed
ensure
viewable_y_offset_valid: Result >= 0 and Result <= height
virtual_height: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
result_non_negative: Result >= 0
virtual_position_changed_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32]]
virtual_x_positionvirtual_y_position
virtual_x_position
virtual_y_position
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
virtual_size_changed_actions: ACTION_SEQUENCE [TUPLE [INTEGER_32, INTEGER_32]]
virtual_widthvirtual_height
virtual_width
virtual_height
EV_GRID_ACTION_SEQUENCES
ensure EV_GRID_ACTION_SEQUENCES
result_not_void: Result /= Void
virtual_width: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
result_non_negative: Result >= 0
virtual_x_position: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
valid_result: Result >= 0 and Result <= maximum_virtual_x_position
virtual_y_position: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
valid_result: Result >= 0 and Result <= maximum_virtual_y_position
feature
cell_client_height: INTEGER_32
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
bridge_ok: Result = implementation.client_height
cell_client_width: INTEGER_32
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
bridge_ok: Result = implementation.client_width
screen_x: INTEGER_32
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.screen_x
screen_y: INTEGER_32
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.screen_y
feature
frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies some.same_type (other)
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure 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
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
are_columns_drawn_above_rows: BOOLEAN
`True'`Current'columnrow
`False'
require
not_destroyed: not is_destroyed
column_displayed (a_column: INTEGER_32): BOOLEAN
`a_column'`Current'
hide`a_column'
`a_column'
require
not_destroyed: not is_destroyed
a_column_within_bounds: a_column > 0 and a_column <= column_count
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
cell_count: INTEGER_32
`Current'
EV_CELL
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure then EV_CELL
valid_result: Result = 0 or Result = 1
cell_extendible: BOOLEAN
EV_CELL`is_empty'
EV_CELL
first_visible_column: EV_GRID_COLUMN
`Current'column_count
is_horizontal_scrolling_per_item
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
has_columns_implies_result_not_void: column_count > 0 implies Result /= Void
no_columns_implies_result_void: column_count = 0 implies Result = Void
first_visible_row: EV_GRID_ROW
`Current'row_count
is_vertical_scrolling_per_item
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
has_rows_implies_result_not_void: row_count > 0 implies Result /= Void
no_rows_implies_result_void: row_count = 0 implies Result = Void
cell_full: BOOLEAN
EV_CELL
has_capture: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_capture
has_focus: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_focus
frozen id_freed: BOOLEAN
`Current'
IDENTIFIED
is_displayed: BOOLEAN
`Current'
`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_displayed
is_dockable: BOOLEAN
`Current'
`True'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_dockable
cell_is_empty: BOOLEAN
EV_CELL`extendible'
EV_CELL
is_external_docking_enabled: BOOLEAN
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_enabled
is_external_docking_relative: BOOLEAN
`Current'
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_relative
cell_is_inserted (v: EV_WIDGET): BOOLEAN
`v'
`has (v)'
COLLECTION
is_multiple_item_selection_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_multiple_row_selection_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_selection_keyboard_handling_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_selection_on_click_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_selection_on_single_button_click_enabled: BOOLEAN
`1'
require
not_destroyed: not is_destroyed
is_sensitive: BOOLEAN
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
bridge_ok: Result = implementation.user_is_sensitive
is_show_requested: BOOLEAN
`Current'
is_displayed
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_show_requested
is_single_item_selection_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_single_row_selection_enabled: BOOLEAN
require
not_destroyed: not is_destroyed
is_tree_enabled: BOOLEAN
`True'`Current'
enable_treedisable_tree
require
not_destroyed: not is_destroyed
last_visible_column: EV_GRID_COLUMN
`Current'column_count
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
has_columns_implies_result_not_void: column_count > 0 implies Result /= Void
no_columns_implies_result_void: column_count = 0 implies Result = Void
last_visible_row: EV_GRID_ROW
`Current'row_count
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
has_rows_implies_result_not_void: row_count > 0 implies Result /= Void
no_rows_implies_result_void: row_count = 0 implies Result = Void
cell_merged_radio_button_groups: ARRAYED_LIST [EV_CONTAINER]
`Result'
`Current'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
not_is_empty: Result /= Void implies not Result.is_empty
mode_is_drag_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_drag_and_drop
mode_is_pick_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_pick_and_drop
mode_is_target_menu: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_target_menu
prunable: BOOLEAN is False
readable: BOOLEAN is False
real_source: EV_DOCKABLE_SOURCE
`Result'
`Current'
`Void'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.real_source
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
tree_node_connector_color: EV_COLOR
`Current'
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
viewable_row_indexes: ARRAYED_LIST [INTEGER_32]
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= Void
visible_column_indexes: ARRAYED_LIST [INTEGER_32]
`Current'
`Result'
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
result_not_void: Result /= Void
visible_row_indexes: ARRAYED_LIST [INTEGER_32]
`Current'
`Result'is_tree_enabled
require
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure
result_not_void: Result /= Void
tree_not_enabled_implies_visible_rows_contiguous: row_count > 0 and then not is_tree_enabled implies Result.last - Result.first = Result.count - 1
writable: BOOLEAN is False
feature
center_pointer
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
disable_always_selected
`Current'
require
not_destroyed: not is_destroyed
ensure
not_is_item_always_selected_enabled: not is_always_selected
disable_capture
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
not_has_capture: not has_capture
disable_column_resize_immediate
is_column_resize_immediate`False'
require
not_destroyed: not is_destroyed
ensure
not_is_column_resize_immediate: not is_column_resize_immediate
disable_column_separators
are_column_separators_enabled`False'
require
not_destroyed: not is_destroyed
ensure
column_separators_disabled: not are_column_separators_enabled
disable_columns_drawn_above_rows
are_columns_drawn_above_rows`False'
require
not_destroyed: not is_destroyed
ensure
columns_drawn_below_rows: not are_columns_drawn_above_rows
disable_dockable
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
not_is_dockable: not is_dockable
disable_docking
is_docking_enabled
`Current'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
not_dockable: not is_docking_enabled
disable_dynamic_content
`Current'
require
not_destroyed: not is_destroyed
ensure
content_not_dynamic: not is_content_partially_dynamic
disable_external_docking
`False'is_external_docking_enabled
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
ensure EV_DOCKABLE_SOURCE
not_externally_dockable: not is_external_docking_enabled
disable_external_docking_relative
`False'is_external_docking_relative
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
external_docking_enabled: is_external_docking_enabled
ensure EV_DOCKABLE_SOURCE
external_docking_not_relative: not is_external_docking_relative
disable_full_redraw_on_virtual_position_change
is_full_redraw_on_virtual_position_change_enabled`False'
require
not_is_destroyed: not is_destroyed
ensure
not_is_full_redraw_on_virtual_position_change_enabled: not is_full_redraw_on_virtual_position_change_enabled
disable_horizontal_overscroll
is_horizontal_overscroll_enabled`False'
require
not_destroyed: not is_destroyed
ensure
not_is_horizontal_overscroll_enabled: not is_horizontal_overscroll_enabled
disable_horizontal_scrolling_per_item
require
not_destroyed: not is_destroyed
ensure
horizontal_scrolling_performed_per_pixel: not is_horizontal_scrolling_per_item
disable_pebble_positioning
`False'pebble_positioning_enabled
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_positioning_updated: not pebble_positioning_enabled
disable_resizing_divider
require
not_destroyed: not is_destroyed
ensure
resizing_divider_disabled: not is_resizing_divider_enabled
disable_row_height_fixed
require
not_destroyed: not is_destroyed
not_dynamic_content_enabled_with_height_not_bounded: not (is_content_partially_dynamic and is_vertical_overscroll_enabled = False)
ensure
row_height_variable: not is_row_height_fixed
disable_row_separators
are_row_separators_enabled`False'
require
not_destroyed: not is_destroyed
ensure
row_separators_disabled: not are_row_separators_enabled
disable_selection_key_handling
require
not_destroyed: not is_destroyed
ensure
selection_key_handling_disabled: not is_selection_keyboard_handling_enabled
disable_selection_on_click
require
not_destroyed: not is_destroyed
ensure
selection_on_click_disabled: not is_selection_on_click_enabled and then not is_selection_on_single_button_click_enabled
disable_sensitive
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
is_unsensitive: not is_sensitive
disable_solid_resizing_divider
require
not_destroyed: not is_destroyed
ensure
dashed_resizing_divider: not is_resizing_divider_solid
disable_tree
`Current'
require
not_destroyed: not is_destroyed
ensure
tree_disabled: not is_tree_enabled
disable_vertical_overscroll
is_vertical_overscroll_enabled`False'
require
not_destroyed: not is_destroyed
dynamic_content_not_enabled_with_variable_row_heights: not (is_content_partially_dynamic and not is_row_height_fixed)
ensure
not_is_vertical_overscroll_enabled: not is_vertical_overscroll_enabled
disable_vertical_scrolling_per_item
require
not_destroyed: not is_destroyed
not_dynamic_content_enabled_with_row_height_variable: not (is_content_partially_dynamic and is_row_height_fixed = False)
ensure
vertical_scrolling_performed_per_pixel: not is_vertical_scrolling_per_item
enable_always_selected
`Current'
require
not_destroyed: not is_destroyed
ensure
item_is_always_selected_enabled: is_always_selected
enable_capture
disable_capture
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure EV_WIDGET
has_capture: has_capture
enable_column_resize_immediate
is_column_resize_immediate`True'
require
not_destroyed: not is_destroyed
ensure
is_column_resize_immediate: is_column_resize_immediate
enable_column_separators
are_column_separators_enabled`True'
require
not_destroyed: not is_destroyed
ensure
column_separators_enabled: are_column_separators_enabled
enable_columns_drawn_above_rows
are_columns_drawn_above_rows`True'
require
not_destroyed: not is_destroyed
ensure
columns_drawn_above_rows: are_columns_drawn_above_rows
enable_dockable
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
is_dockable: is_dockable
enable_docking
is_docking_enabled
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
is_dockable: is_docking_enabled
enable_external_docking
`True'is_external_docking_enabled
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
ensure EV_DOCKABLE_SOURCE
is_externally_dockable: is_external_docking_enabled
enable_external_docking_relative
`True'is_external_docking_relative
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
external_docking_enabled: is_external_docking_enabled
ensure EV_DOCKABLE_SOURCE
external_docking_not_relative: is_external_docking_relative
enable_full_redraw_on_virtual_position_change
is_full_redraw_on_virtual_position_change_enabled`True'
require
not_is_destroyed: not is_destroyed
ensure
is_full_redraw_on_virtual_position_change_enabled: is_full_redraw_on_virtual_position_change_enabled
enable_horizontal_overscroll
is_horizontal_overscroll_enabled`True'
require
not_destroyed: not is_destroyed
ensure
is_horizontal_overscroll_enabled: is_horizontal_overscroll_enabled
enable_horizontal_scrolling_per_item
require
not_destroyed: not is_destroyed
ensure
horizontal_scrolling_performed_per_item: is_horizontal_scrolling_per_item
enable_multiple_item_selection
require
not_destroyed: not is_destroyed
ensure
multiple_item_selection_enabled: is_multiple_item_selection_enabled
enable_multiple_row_selection
require
not_destroyed: not is_destroyed
ensure
multiple_row_selection_enabled: is_multiple_row_selection_enabled
enable_partial_dynamic_content
`Current'
dynamic_content_function
`Current'
require
not_destroyed: not is_destroyed
not_row_height_variable_and_vertical_overscroll_enabled: not (not is_row_height_fixed and is_vertical_overscroll_enabled)
not_row_height_variable_and_vertical_scrolling_per_pixel: not (not is_row_height_fixed and not is_vertical_scrolling_per_item)
ensure
content_partially_dynamic: is_content_partially_dynamic
enable_pebble_positioning
`True'pebble_positioning_enabled
pebble_x_positionpebble_y_position
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_positioning_updated: pebble_positioning_enabled
enable_resizing_divider
require
not_destroyed: not is_destroyed
ensure
resizing_divider_enabled: is_resizing_divider_enabled
enable_row_height_fixed
require
not_destroyed: not is_destroyed
ensure
row_height_fixed: is_row_height_fixed
enable_row_separators
are_row_separators_enabled`True'
require
not_destroyed: not is_destroyed
ensure
row_separators_enabled: are_row_separators_enabled
enable_selection_key_handling
require
not_destroyed: not is_destroyed
ensure
selection_key_handling_enabled: is_selection_keyboard_handling_enabled
enable_selection_on_click
require
not_destroyed: not is_destroyed
ensure
selection_on_click_enabled: is_selection_on_click_enabled
selection_on_single_click_disabled: not is_selection_on_single_button_click_enabled
enable_selection_on_single_button_click
`1'
`3'
require
not_destroyed: not is_destroyed
ensure
selection_on_single_click_enabled: is_selection_on_single_button_click_enabled and then is_selection_on_click_enabled
enable_sensitive
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
is_sensitive: (parent = Void or parent_is_sensitive) implies is_sensitive
enable_single_item_selection
require
not_destroyed: not is_destroyed
ensure
single_item_selection_enabled: is_single_item_selection_enabled
enable_single_row_selection
require
not_destroyed: not is_destroyed
ensure
single_row_selection_enabled: is_single_row_selection_enabled
enable_solid_resizing_divider
require
not_destroyed: not is_destroyed
ensure
solid_resizing_divider: is_resizing_divider_solid
enable_tree
`Current'
require
not_destroyed: not is_destroyed
ensure
tree_enabled: is_tree_enabled
enable_vertical_overscroll
is_vertical_overscroll_enabled`True'
require
not_destroyed: not is_destroyed
ensure
is_vertical_overscroll_enabled: is_vertical_overscroll_enabled
enable_vertical_scrolling_per_item
require
not_destroyed: not is_destroyed
ensure
vertical_scrolling_performed_per_item: is_vertical_scrolling_per_item
hide
`Current'
is_show_requested`False'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
hide_column (a_column: INTEGER_32)
`a_column'`Current'
require
not_destroyed: not is_destroyed
a_column_within_bounds: a_column > 0 and a_column <= column_count
ensure
column_not_displayed: not column_displayed (a_column)
hide_header
require
not_destroyed: not is_destroyed
ensure
header_not_displayed: not is_header_displayed
hide_horizontal_scroll_bar
`Current'
require
not_is_destroyed: not is_destroyed
ensure
not_is_horizontal_scroll_bar_show_requested: not is_horizontal_scroll_bar_show_requested
hide_tree_node_connectors
`Current'
require
not_destroyed: not is_destroyed
ensure
tree_node_connectors_hidden: not are_tree_node_connectors_shown
hide_vertical_scroll_bar
`Current'
require
not_is_destroyed: not is_destroyed
ensure
not_is_vertical_scroll_bar_show_requested: not is_vertical_scroll_bar_show_requested
is_always_selected: BOOLEAN
`True'
require
not_destroyed: not is_destroyed
is_horizontal_scroll_bar_show_requested: BOOLEAN
`Current'
virtual_widthviewable_width
require
not_is_destroyed: not is_destroyed
is_vertical_scroll_bar_show_requested: BOOLEAN
`Current'
virtual_heightviewable_height
require
not_is_destroyed: not is_destroyed
lock_update
is_locked`True'
unlock_update
require
not_is_destroyed: not is_destroyed
ensure
is_locked: is_locked
cell_merge_radio_button_groups (other: EV_CONTAINER)
`Current'`other'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
other_not_void: other /= Void
redraw
`Current'
require
not_destroyed: not is_destroyed
remove_default_key_processing_handler
default_key_processing_handler
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
default_key_processing_handler_removed: default_key_processing_handler = Void
remove_pebble
pebble`Void'pebble_function
EV_PICK_AND_DROPABLE
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_removed: pebble = Void and pebble_function = Void
remove_real_source
real_source`Void'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
real_source_void: real_source = Void
remove_real_target
real_target`Void'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
real_target_void: real_target = Void
select_column (a_column: INTEGER_32)
`a_column'
require
not_destroyed: not is_destroyed
a_column_within_bounds: a_column > 0 and a_column <= column_count
column_displayed: column_displayed (a_column)
ensure
column_selected: column (a_column).is_selected
select_row (a_row: INTEGER_32)
`a_row'
require
not_destroyed: not is_destroyed
a_row_within_bounds: a_row > 0 and a_row <= row_count
ensure
row_selected: row (a_row).is_selected
set_accept_cursor (a_cursor: like accept_cursor)
`a_cursor'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_cursor_not_void: a_cursor /= Void
ensure 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)
`an_agent'actual_drop_target_agent
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
an_agent_not_void: an_agent /= Void
ensure EV_WIDGET
assigned: actual_drop_target_agent = an_agent
set_column_count_to (a_column_count: INTEGER_32)
`Current'`a_column_count'
require
not_destroyed: not is_destroyed
a_column_count_positive: a_column_count >= 0
ensure
column_count_set: column_count = a_column_count
set_default_colors
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
set_default_key_processing_handler (a_handler: like default_key_processing_handler)
default_key_processing_handler`a_handler'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
set_deny_cursor (a_cursor: like deny_cursor)
`a_cursor'
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_cursor_not_void: a_cursor /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
deny_cursor_assigned: deny_cursor.is_equal (a_cursor)
set_drag_and_drop_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
drag_and_drop_set: mode_is_drag_and_drop
set_dynamic_content_function (a_function: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_GRID_ITEM])
is_content_partially_dynamic
require
not_destroyed: not is_destroyed
a_function_not_void: a_function /= Void
ensure
dynamic_content_function_set: dynamic_content_function = a_function
set_first_visible_row (a_row: INTEGER_32)
`a_row'`Current'
`a_row'`Current'
require
not_destroyed: not is_destroyed
valid_row_index: a_row >= 1 and a_row <= row_count
ensure
to_implement_assertion ("EV_GRID.set_first_visible_row - Enough following rows implies `first_visible_row' = a_row, Can be calculated from `height' of `Current' and row heights.")
set_focus
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
is_sensitive: is_sensitive
set_focused_selection_color (a_color: EV_COLOR)
`a_color'focused_selection_color
require
not_is_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
focused_selection_color_set: focused_selection_color = a_color
set_focused_selection_text_color (a_color: EV_COLOR)
`a_color'focused_selection_text_color
require
not_is_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
focused_selection_text_color_set: focused_selection_text_color = a_color
set_item_accept_cursor_function (a_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], EV_POINTER_STYLE])
`a_function'item_accept_cursor_function
require
not_destroyed: not is_destroyed
ensure
item_accept_cursor_function_set: item_accept_cursor_function = a_function
set_item_deny_cursor_function (a_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], EV_POINTER_STYLE])
`a_function'item_deny_cursor_function
require
not_destroyed: not is_destroyed
ensure
item_deny_cursor_function_set: item_deny_cursor_function = a_function
set_item_pebble_function (a_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM], ANY])
`a_function'item_pebble_function
require
not_destroyed: not is_destroyed
ensure
item_pebble_function_set: item_pebble_function = a_function
set_item_veto_pebble_function (a_function: FUNCTION [ANY, TUPLE [EV_GRID_ITEM, ANY], BOOLEAN])
`a_function'item_veto_pebble_function
require
not_destroyed: not is_destroyed
ensure
item_veto_pebble_function_set: item_veto_pebble_function = a_function
set_node_pixmaps (an_expand_node_pixmap, a_collapse_node_pixmap: EV_PIXMAP)
`an_expand_node_pixmap'expand_node_pixmap`a_collapse_node_pixmap'
collapse_node_pixmap
require
not_destroyed: not is_destroyed
pixmaps_not_void: an_expand_node_pixmap /= Void and a_collapse_node_pixmap /= Void
pixmaps_dimensions_identical: an_expand_node_pixmap.width = a_collapse_node_pixmap.width and an_expand_node_pixmap.height = a_collapse_node_pixmap.height
ensure
pixmaps_set: expand_node_pixmap = an_expand_node_pixmap and collapse_node_pixmap = a_collapse_node_pixmap
set_non_focused_selection_color (a_color: EV_COLOR)
`a_color'non_focused_selection_color
require
not_is_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
non_focused_selection_color_set: non_focused_selection_color = a_color
set_non_focused_selection_text_color (a_color: EV_COLOR)
`a_color'non_focused_selection_text_color
require
not_is_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
non_focused_selection_text_color_set: non_focused_selection_text_color = a_color
set_pebble (a_pebble: like pebble)
`a_pebble'pebble
set_pebble_function
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_pebble_not_void: a_pebble /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_assigned: pebble = a_pebble
set_pebble_function (a_function: FUNCTION [ANY, TUPLE, ANY])
`a_function'pebble
pebble
`a_function'
set_pebble
EV_PICK_AND_DROPABLE
require 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 EV_ABSTRACT_PICK_AND_DROPABLE
pebble_function_assigned: pebble_function = a_function
set_pebble_position (a_x, a_y: INTEGER_32)
`Current'
`True'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y
set_pick_and_drop_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pick_and_drop_set: mode_is_pick_and_drop
set_real_source (dockable_source: EV_DOCKABLE_SOURCE)
`dockable_source'real_source
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
dockable_source_not_void: dockable_source /= Void
dockable_source_is_parent_recursive: source_has_current_recursive (dockable_source)
ensure EV_DOCKABLE_SOURCE
real_source_assigned: real_source = dockable_source
set_real_target (a_target: EV_DOCKABLE_TARGET)
`a_target'real_target
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
target_not_void: a_target /= Void
ensure EV_WIDGET
assigned: real_target = a_target
set_row_count_to (a_row_count: INTEGER_32)
`Current'`a_row_count'
require
not_destroyed: not is_destroyed
a_row_count_non_negative: a_row_count >= 0
ensure
row_count_set: row_count = a_row_count
set_row_height (a_row_height: INTEGER_32)
`Current'
is_row_height_fixed
require
not_destroyed: not is_destroyed
is_row_height_fixed: is_row_height_fixed
a_row_height_positive: a_row_height >= 1
ensure
row_height_set: row_height = a_row_height
set_separator_color (a_color: EV_COLOR)
`a_color'separator_color
require
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
separator_color_set: separator_color = a_color
set_subrow_indent (a_subrow_indent: INTEGER_32)
subrow_indent`a_subrow_indent'
require
not_destroyed: not is_destroyed
a_subrow_indent_non_negtive: a_subrow_indent >= 0
ensure
subrow_indent_set: subrow_indent = a_subrow_indent
set_target_menu_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
target_menu_mode_set: mode_is_target_menu
set_target_name (a_name: STRING_GENERAL)
`a_name'target_name
EV_ABSTRACT_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_name_not_void: a_name /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
target_name_assigned: a_name /= target_name and a_name.is_equal (target_name)
set_tree_node_connector_color (a_color: EV_COLOR)
`a_color'tree_node_connector_color
require
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure
tree_node_connector_color_set: tree_node_connector_color = a_color
set_veto_dock_function (a_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN])
`a_function'veto_dock_function
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
a_function_not_void: a_function /= Void
ensure EV_DOCKABLE_TARGET
veto_function_set: veto_dock_function = a_function
set_virtual_position (virtual_x, virtual_y: INTEGER_32)
`Current'`virtual_x'`virtual_y'
require
not_destroyed: not is_destroyed
virtual_x_valid: virtual_x >= 0 and virtual_x <= maximum_virtual_x_position
virtual_y_valid: virtual_y >= 0 and virtual_y <= maximum_virtual_y_position
ensure
virtual_position_set: virtual_x_position = virtual_x and virtual_y_position = virtual_y
show
`Current'
`True'
is_show_requested`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
show_column (a_column: INTEGER_32)
`a_column'`Current'
require
not_destroyed: not is_destroyed
a_column_within_bounds: a_column > 0 and a_column <= column_count
ensure
column_displayed: column_displayed (a_column)
show_header
require
not_destroyed: not is_destroyed
ensure
header_displayed: is_header_displayed
show_horizontal_scroll_bar
`Current'
virtual_width
viewable_width
require
not_is_destroyed: not is_destroyed
ensure
is_horizontal_scroll_bar_show_requested: is_horizontal_scroll_bar_show_requested
show_tree_node_connectors
`Current'
require
not_destroyed: not is_destroyed
ensure
tree_node_connectors_shown: are_tree_node_connectors_shown
show_vertical_scroll_bar
`Current'
virtual_height
viewable_height
require
not_is_destroyed: not is_destroyed
ensure
is_vertical_scroll_bar_show_requested: is_vertical_scroll_bar_show_requested
unlock_update
is_locked`False'
require
not_is_destroyed: not is_destroyed
ensure
not_is_locked: not is_locked
cell_unmerge_radio_button_groups (other: EV_CONTAINER)
`other'`Current'
`other'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
other_is_merged: cell_merged_radio_button_groups.has (other)
ensure EV_CONTAINER
other_not_merged: other.merged_radio_button_groups = Void
not_contained_in_this_group: cell_merged_radio_button_groups /= Void implies not cell_merged_radio_button_groups.has (other)
other_first_radio_button_now_selected: not old other.has_selected_radio_button and old other.has_radio_button implies other.first_radio_button_selected
original_radio_button_still_selected: old cell_has_selected_radio_button implies cell_has_selected_radio_button
other_first_radio_button_now_selected: not old cell_has_selected_radio_button and old other.has_radio_button and old cell_merged_radio_button_groups.count = 1 and cell_has_radio_button implies cell_first_radio_button_selected
other_original_radio_button_still_selected: old other.has_selected_radio_button implies other.has_selected_radio_button
feature
clear
`Current'
require
not_destroyed: not is_destroyed
ensure
to_implement_assertion ("EV_GRID.clear - All items positions return `Void'.")
cell_extend (v: like cell_item)
`v'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
extendible: cell_extendible
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: v /= Current
v_not_parent_of_current: not cell_is_parent_recursive (v)
v_containable: cell_may_contain (v)
ensure EV_CONTAINER
has_v: cell_has (v)
cell_fill (other: CONTAINER [EV_WIDGET])
`other'
`other'
COLLECTION
require COLLECTION
other_not_void: other /= Void
extendible: cell_extendible
insert_new_column (a_index: INTEGER_32)
`a_index'
require
not_destroyed: not is_destroyed
a_index_within_range: a_index > 0 and a_index <= column_count + 1
new_column_insertable: a_index <= column_count implies column ((a_index - 1).max (1)).all_items_may_be_set
ensure
column_count_set: column_count = old column_count + 1
insert_new_row (i: INTEGER_32)
`i'
require
not_destroyed: not is_destroyed
i_within_range: i > 0 and i <= row_count + 1
not_inserting_within_existing_subrow_structure: i <= row_count implies row (i).parent_row = Void
ensure
row_count_set: row_count = old row_count + 1
insert_new_row_parented (i: INTEGER_32; a_parent_row: EV_GRID_ROW)
`i'`a_parent_row'
require
not_destroyed: not is_destroyed
tree_enabled: is_tree_enabled
i_positive: i > 0
i_less_than_row_count: i <= row_count + 1
a_parent_row_not_void: a_parent_row /= Void
a_parent_row_in_current: a_parent_row.parent = Current
i_valid_for_parent: i > a_parent_row.index and i <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1
not_inserting_within_existing_subrow_structure: i < a_parent_row.index + a_parent_row.subrow_count_recursive implies row (i).parent_row = a_parent_row
ensure
row_count_set: row_count = old row_count + 1
subrow_count_set: a_parent_row.subrow_count = old a_parent_row.subrow_count + 1
insert_new_rows (rows_to_insert, i: INTEGER_32)
`rows_to_insert'`i'
require
not_destroyed: not is_destroyed
i_within_range: i > 0 and i <= row_count + 1
rows_to_insert_positive: rows_to_insert >= 1
not_inserting_within_existing_subrow_structure: i <= row_count implies row (i).parent_row = Void
ensure
row_count_set: row_count = old row_count + rows_to_insert
insert_new_rows_parented (rows_to_insert, i: INTEGER_32; a_parent_row: EV_GRID_ROW)
`rows_to_insert'`i'
`a_parent_row'
require
not_destroyed: not is_destroyed
tree_enabled: is_tree_enabled
i_positive: i > 0
rows_to_insert_positive: rows_to_insert >= 1
i_less_than_row_count: i <= row_count + 1
a_parent_row_not_void: a_parent_row /= Void
i_valid_for_parent: i > a_parent_row.index and i <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1
not_inserting_within_existing_subrow_structure: i < a_parent_row.index + a_parent_row.subrow_count_recursive implies row (i).parent_row = a_parent_row
ensure
row_count_set: row_count = old row_count + rows_to_insert
subrow_count_set: a_parent_row.subrow_count = old a_parent_row.subrow_count + rows_to_insert
move_column (i, j: INTEGER_32)
`i'`j'
`i'`j'`column_count + 1'
require
not_destroyed: not is_destroyed
i_valid: i > 0 and then i <= column_count
j_valid: j > 0 and then j <= column_count + 1
column_i_moveable: column (i).all_items_may_be_removed
column_j_settable: j <= column_count implies column (j).all_items_may_be_set
ensure
columns_moved: (j <= i implies column (j) = old column (i)) and (j > i implies column (j - 1) = old column (i)) and (j < i implies (column (i) = old column ((i - 1).max (1)))) and (j > i + 1 implies (column (i) = old column ((i + 1).min (column_count))))
column_count_unchanged: column_count = old column_count
move_columns (i, j, n: INTEGER_32)
`n'`i'`j'
require
not_destroyed: not is_destroyed
i_valid: i > 0 and then i <= column_count
j_valid: j > 0 and then j <= column_count + 1
n_valid: n > 0 and then i + n <= column_count + 1
move_not_overlapping: n > 1 implies (j <= i or else j >= i + n)
columns_removable: are_columns_removable (i, n)
column_j_settable: j <= column_count implies column (j).all_items_may_be_set
ensure
columns_moved: (j < i implies column (j) = old column (i) and then column (j + n - 1) = old column (i + n - 1)) and (j > i + n implies column (j - n) = old column (i) and then column (j - 1) = old column (i + n - 1))
column_count_unchanged: column_count = old column_count
move_row (i, j: INTEGER_32)
`i'`j'
`j'`row_count + 1'`i'
`i'`parent_row'
require
not_destroyed: not is_destroyed
i_valid: i > 0 and then i <= row_count
j_valid: j > 0 and then j <= row_count + 1
row_has_no_subrows: row (i).subrow_count = 0
not_breaking_existing_subrow_structure: j = row_count + 1 or (j = i or (j = i + 1 and (i + 1 <= row_count)) and then row (i + 1).parent_row = Void) or row (j).parent_row = Void
ensure
rows_moved: (j <= i implies row (j) = old row (i)) and (j > i implies row (j - 1) = old row (i)) and (j < i implies (row (i) = old row ((i - 1).max (1)))) and (j > i + 1 implies (row (i) = old row ((i + 1).min (row_count))))
row_count_unchanged: row_count = old row_count
move_row_to_parent (i, j: INTEGER_32; a_parent_row: EV_GRID_ROW)
`i'`j'
`i'`a_parent_row'
`j'`row_count + 1'`i'
require
not_destroyed: not is_destroyed
tree_enabled: is_tree_enabled
i_valid: i > 0 and then i <= row_count
j_valid: j > 0 and then j <= row_count + 1
row_has_no_subrows: row (i).subrow_count = 0
a_parent_row_not_void: a_parent_row /= Void
j_valid_for_move_to_a_parent_row: (j = i + 1 implies (i > a_parent_row.index and i <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1)) or (j > a_parent_row.index and j <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1)
rows_may_be_moved: rows_may_be_moved (i, 1)
not_inserting_within_existing_subrow_structure: j < a_parent_row.index + a_parent_row.subrow_count_recursive implies row (j).parent_row = a_parent_row
ensure
rows_moved: (j <= i implies row (j) = old row (i)) and (j > i implies row (j - 1) = old row (i)) and (j < i implies (row (i) = old row ((i - 1).max (1)))) and (j > i + 1 implies (row (i) = old row ((i + 1).min (row_count))))
row_count_unchanged: row_count = old row_count
move_rows (i, j, n: INTEGER_32)
`n'`i'`j'
`j'`row_count + 1'
is_tree_enabled
`i'
`i'
require
not_destroyed: not is_destroyed
i_valid: i > 0 and then i <= row_count
j_valid: j > 0 and then j <= row_count + 1
n_valid: n > 0 and then i + n <= row_count + 1
move_not_overlapping: n > 1 implies (j <= i or else j >= i + n)
rows_may_be_moved: rows_may_be_moved (i, n)
not_breaking_existing_subrow_structure: j = row_count + 1 or (j = i or (j = i + n and (i + n <= row_count)) and then row (i + n).parent_row = Void) or row (j).parent_row = Void
ensure
rows_moved: (j <= i implies row (j) = old row (i) and then row (j + n - 1) = old row (i + n - 1)) and (j > i + n implies row (j - n) = old row (i) and then row (j - 1) = old row (i + n - 1))
row_count_unchanged: row_count = old row_count
move_rows_to_parent (i, j, n: INTEGER_32; a_parent_row: EV_GRID_ROW)
`n'`i'`j'
`i'`a_parent_row'
`i'
require
not_destroyed: not is_destroyed
tree_enabled: is_tree_enabled
i_valid: i > 0 and then i <= row_count
j_valid: j > 0 and then j <= row_count + 1
n_valid: n > 0 and then i + n <= row_count + 1
move_not_overlapping: n > 1 implies (j <= i or else j >= i + n)
rows_may_be_moved: rows_may_be_moved (i, n)
a_parent_row_not_void: a_parent_row /= Void
j_valid_for_move_to_a_parent_row: (j = i + n implies (i > a_parent_row.index and i <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1)) or (j > a_parent_row.index and j <= a_parent_row.index + a_parent_row.subrow_count_recursive + 1)
not_inserting_within_existing_subrow_structure: j <= a_parent_row.index + a_parent_row.subrow_count_recursive implies row (j).parent_row = a_parent_row
ensure
rows_moved: (j < i implies row (j) = old row (i) and then row (j + n - 1) = old row (i + n - 1)) and (j > i + n implies row (j - n) = old row (i) and then row (j - 1) = old row (i + n - 1))
row_count_unchanged: row_count = old row_count
cell_put (v: like cell_item)
item`v'
EV_CONTAINER`replace'
EV_CONTAINER
require 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 cell_is_parent_recursive (v)
v_containable: cell_may_contain (v)
ensure EV_CONTAINER
has_v: cell_has (v)
not_has_old_item: not cell_has (old cell_item)
remove_help_context
`EV_APPLICATION.help_key'
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
help_context_not_void: help_context /= Void
ensure EV_HELP_CONTEXTABLE
no_help_context: help_context = Void
remove_item (a_column, a_row: INTEGER_32)
`a_column'`a_row'
require
not_destroyed: not is_destroyed
a_column_positive: a_column > 0
a_row_positive: a_row > 0
item_may_be_removed_if_row_is_a_subrow: row (a_row).is_part_of_tree_structure implies row (a_row).is_index_valid_for_item_removal_if_tree_node (a_column)
ensure
item_removed: item (a_column, a_row) = Void
remove_background_pixmap
`Current'
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
pixmap_removed: cell_background_pixmap = Void
remove_tooltip
tooltip
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
tooltip_removed: tooltip.is_empty
cell_replace (v: like cell_item)
item`v'
EV_CONTAINER`put'
EV_CONTAINER
require 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 cell_is_parent_recursive (v)
v_containable: cell_may_contain (v)
ensure EV_CONTAINER
has_v: cell_has (v)
not_has_old_item: not cell_has (old cell_item)
set_background_color (a_color: like background_color)
`a_color'background_color
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure EV_COLORIZABLE
background_color_assigned: background_color.is_equal (a_color)
set_data (some_data: like data)
`some_data'data
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
set_foreground_color (a_color: like foreground_color)
`a_color'foreground_color
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure EV_COLORIZABLE
foreground_color_assigned: foreground_color.is_equal (a_color)
set_help_context (an_help_context: like help_context)
`an_help_context'help_context
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
an_help_context_not_void: an_help_context /= Void
ensure EV_HELP_CONTEXTABLE
help_context_assigned: help_context.is_equal (an_help_context)
set_item (a_column, a_row: INTEGER_32; a_item: EV_GRID_ITEM)
`a_column'`a_row'`a_item'
`a_item'`Void'
require
not_destroyed: not is_destroyed
a_item_not_parented: a_item /= Void implies a_item.parent = Void
a_column_positive: a_column > 0
a_row_positive: a_row > 0
item_may_be_added_if_row_is_a_subrow: a_item /= Void and then a_row <= row_count and then row (a_row).is_part_of_tree_structure implies row (a_row).is_index_valid_for_item_setting_if_tree_node (a_column)
item_may_be_removed_if_row_is_a_subrow: a_item = Void and then a_row <= row_count and then row (a_row).is_part_of_tree_structure implies row (a_row).is_index_valid_for_item_removal_if_tree_node (a_column)
ensure
item_set: item (a_column, a_row) = a_item
set_minimum_height (a_minimum_height: INTEGER_32)
`a_minimum_height'minimum_height
height`a_minimum_height'
minimum_height
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_height_positive: a_minimum_height >= 0
ensure EV_WIDGET
minimum_height_assigned: minimum_height = a_minimum_height
minimum_height_set_by_user_set: minimum_height_set_by_user
set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32)
`a_minimum_height'minimum_height
`a_minimum_width'minimum_width
widthheight
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width >= 0
a_minimum_height_positive: a_minimum_height >= 0
ensure EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width
minimum_height_assigned: minimum_height = a_minimum_height
minimum_height_set_by_user_set: minimum_height_set_by_user
minimum_width_set_by_user_set: minimum_width_set_by_user
set_minimum_width (a_minimum_width: INTEGER_32)
`a_minimum_width'minimum_width
width`a_minimum_width'
minimum_width
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width >= 0
ensure EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width
minimum_width_set_by_user_set: minimum_width_set_by_user
set_background_pixmap (a_pixmap: EV_PIXMAP)
`a_pixmap'`Current'
`pixmap'`a_pixmap'
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
pixmap_not_void: a_pixmap /= Void
set_pointer_style (a_cursor: like pointer_style)
`a_cursor'pointer_style
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_cursor_not_void: a_cursor /= Void
ensure EV_WIDGET
pointer_style_assigned: pointer_style.is_equal (a_cursor)
set_tooltip (a_tooltip: STRING_GENERAL)
`a_tooltip'tooltip
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
tooltip: a_tooltip /= Void
ensure EV_TOOLTIPABLE
tooltip_assigned: tooltip.is_equal (a_tooltip)
cloned: tooltip /= a_tooltip
wipe_out
`Current'
require
not_destroyed: not is_destroyed
ensure
columns_removed: column_count = 0
rows_removed: row_count = 0
feature
frozen free_id
object_id
IDENTIFIED
ensure IDENTIFIED
object_freed: id_freed
cell_prune (v: EV_WIDGET)
`v'
EV_CELL
require COLLECTION
prunable: prunable
ensure then EV_CELL
not cell_has (v)
cell_prune_all (v: EV_WIDGET)
`v'
object_comparison
COLLECTION
require COLLECTION
prunable: prunable
ensure COLLECTION
no_more_occurrences: not cell_has (v)
remove_column (a_column: INTEGER_32)
`a_column'
require
not_destroyed: not is_destroyed
a_column_positive: a_column > 0
a_column_less_than_column_count: a_column <= column_count
column_may_be_removed: column (a_column).all_items_may_be_removed
ensure
column_count_updated: column_count = old column_count - 1
old_column_removed: (old column (a_column)).parent = Void
remove_row (a_row: INTEGER_32)
`a_row'
`row (a_row).subrow_count_recursive'
`Current'
require
not_destroyed: not is_destroyed
a_row_positive: a_row > 0
a_row_less_than_row_count: a_row <= row_count
ensure
row_count_updated: row_count = old row_count - (old row (a_row).subrow_count_recursive + 1)
old_row_removed: (old row (a_row)).parent = Void
to_implement_assertion ("EV_GRID.remove_row%T%TAll old recursive subrows removed.")
remove_rows (lower_index, upper_index: INTEGER_32)
`lower_index'`upper_index'
require
not_destroyed: not is_destroyed
valid_lower_index: lower_index >= 1 and lower_index <= row_count
valid_upper_index: upper_index >= lower_index and upper_index <= row_count
valid_final_row_in_tree_structure: is_tree_enabled and then highest_parent_row_within_bounds (lower_index, upper_index) /= Void implies upper_index = highest_parent_row_within_bounds (lower_index, upper_index).index + highest_parent_row_within_bounds (lower_index, upper_index).subrow_count_recursive
ensure
row_count_consistent: row_count = (old row_count) - (upper_index - lower_index + 1)
lower_row_removed: (old row (lower_index)).parent = Void
upper_row_removed: (old row (upper_index)).parent = Void
to_implement_assertion (once "middle_rows_removed from lower to upper all old rows parent = Void")
cell_wipe_out
item
EV_CELL
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: cell_is_empty
feature
cell_linear_representation: LINEAR [like cell_item]
EV_CELL
feature
copy (other: like Current)
`other'
EV_ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: like Current)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: like Current
ANY
ensure ANY
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: like Current
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
cell_propagate_background_color
background_color
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
background_color_propagated: cell_background_color_propagated
cell_propagate_foreground_color
foreground_color
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
foreground_color_propagated: cell_foreground_color_propagated
refresh_now
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
feature
column_type: EV_GRID_COLUMN
EV_GRID_TYPES
row_type: EV_GRID_ROW
EV_GRID_TYPES
feature
destroy
`Current'
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
are_columns_removable (a_index, n: INTEGER_32): BOOLEAN
`n'`a_index'`Current'
require
a_index_positive: a_index > 0
n_positive: n > 0
a_index_not_greater_than_column_count: a_index <= column_count
n_valid: a_index + n <= column_count + 1
highest_parent_row_within_bounds (lower_index, upper_index: INTEGER_32): EV_GRID_ROW
`parent_row'`upper_index'
`lower_index'
require
not_destroyed: not is_destroyed
tree_enabled: is_tree_enabled
valid_lower_index: lower_index >= 1 and lower_index <= row_count
valid_upper_index: upper_index >= lower_index and upper_index <= row_count
ensure
result_not_void: Result /= Void
cell_is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
`a_widget'parentparentparent
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
cell_may_contain (v: EV_WIDGET): BOOLEAN
`v'`Current'
EV_CONTAINER
parent_of_source_allows_docking: BOOLEAN
real_source
EV_DOCKABLE_SOURCE
rows_may_be_moved (a_first_row_index, a_row_count: INTEGER_32): BOOLEAN
`a_first_row_index'`a_first_row_index'`a_row_count'
`a_first_row_index'`parent_row'
`Result'`True'
require
row_count_positive: a_row_count >= 1
first_row_index_valid: a_first_row_index >= 1 and a_first_row_index + a_row_count - 1 <= row_count
source_has_current_recursive (source: EV_DOCKABLE_SOURCE): BOOLEAN
`source'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
source_not_void: source /= Void
feature
conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE
`Current'
EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
ensure EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
not_void: Result /= Void
dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
ensure EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
not_void: Result /= Void
docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE
EV_DOCKABLE_TARGET_ACTION_SEQUENCES
ensure EV_DOCKABLE_TARGET_ACTION_SEQUENCES
not_void: Result /= Void
drop_actions: EV_PND_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_press_actions: EV_KEY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_release_actions: EV_KEY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pick_actions: EV_PND_START_ACTION_SEQUENCE
pebble
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE
`Current'
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
feature
fixme (comment: STRING_8)
`comment'
REFACTORING_HELPER
require REFACTORING_HELPER
comment_not_void: comment /= Void
to_implement (comment: STRING_8)
`comment'
REFACTORING_HELPER
require REFACTORING_HELPER
comment_not_void: comment /= Void
to_implement_assertion (comment: STRING_8): BOOLEAN
`comment'
REFACTORING_HELPER
require REFACTORING_HELPER
comment_not_void: comment /= Void
feature
height: INTEGER_32
minimum_height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.height
minimum_height: INTEGER_32
height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_height
positive_or_zero: Result >= 0
minimum_width: INTEGER_32
width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_width
positive_or_zero: Result >= 0
width: INTEGER_32
minimum_width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.width
x_position: INTEGER_32
x_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.x_position
y_position: INTEGER_32
y_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.y_position
feature
column_count: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
result_not_negative: Result >= 0
displayed_column_count: INTEGER_32
column_count
hide
require
not_destroyed: not is_destroyed
ensure
result_valid: Result >= 0 and Result <= column_count
row_count: INTEGER_32
require
not_destroyed: not is_destroyed
ensure
result_not_negative: Result >= 0
tree_node_spacing: INTEGER_32
row_height
require
not_destroyed: not is_destroyed
ensure
result_positive: Result >= 1
feature
io: STD_FILES
ANY
out: STRING_8
ANYtagged_out
ANY
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
feature
is_destroyed: BOOLEAN
`Current'
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
EV_CONTAINER
client_width_within_bounds: is_usable implies cell_client_width >= 0 and cell_client_width <= width
client_height_within_bounds: is_usable implies cell_client_height >= 0 and cell_client_height <= height
all_radio_buttons_connected: is_usable implies cell_all_radio_buttons_connected
parent_of_items_is_current: is_usable implies cell_parent_of_items_is_current
items_unique: is_usable implies cell_items_unique
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)
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
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= Void and then implementation.interface = Current
default_create_called: default_create_called
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_DOCKABLE_SOURCE
parent_permits_docking: is_dockable implies parent_of_source_allows_docking
EV_COLORIZABLE
background_color_not_void: is_usable implies background_color /= Void
foreground_color_not_void: is_usable implies foreground_color /= Void
EV_POSITIONED
width_not_negative: is_usable implies width >= 0
height_not_negative: is_usable implies height >= 0
minimum_width_not_negative: is_usable implies minimum_width >= 0
minimum_height_not_negative: is_usable implies minimum_height >= 0
indexing
copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
source: "[
Eiffel Software
356 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Website http://www.eiffel.com
Customer support http://support.eiffel.com
]"
end EV_GRID