Automatic generation produced by ISE Eiffel
note 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`. Separators 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 occurring 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: 2016-09-27 07:50:48 -0800 (Tue, 27 Sep 2016) $" revision: "$Revision: 99192 $" class interface EV_GRID create default_create -- Standard creation procedure. -- (from EV_ANY) require -- from ANY True ensure then -- from EV_ANY is_coupled: implementation /= Void is_initialized: is_initialized default_create_called: default_create_called is_in_default_state: is_in_default_state feature -- Access accept_cursor: EV_POINTER_STYLE -- Result is cursor displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE result_not_void: Result /= Void ensure then -- from EV_PICK_AND_DROPABLE cursor_valid: (attached implementation.accept_cursor implies Result = implementation.accept_cursor) or else Result = Default_pixmaps.Standard_cursor activated_item: detachable EV_GRID_ITEM -- Item that has currently been activated, if any. require not_destroyed: not is_destroyed actual_drop_target_agent: detachable FUNCTION [INTEGER_32, INTEGER_32, detachable EV_ABSTRACT_PICK_AND_DROPABLE] -- Overrides default drop target on a certain position. -- If Void, Current will use the default drop target. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.actual_drop_target_agent are_column_separators_enabled: BOOLEAN -- Is a vertical separator displayed in color `separator_color` between each column? require not_destroyed: not is_destroyed are_row_separators_enabled: BOOLEAN -- Is a horizontal separator displayed in color `separator_color` between each row? require not_destroyed: not is_destroyed are_tree_node_connectors_shown: BOOLEAN -- Are connectors between tree nodes shown in Current? require not_destroyed: not is_destroyed background_color: EV_COLOR -- Color displayed behind foreground features. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed ensure -- from EV_COLORIZABLE bridge_ok: Result.is_equal (implementation.background_color) cell_background_pixmap: detachable EV_PIXMAP -- Result is pixmap displayed on background of Current. -- It is tessellated and fills whole of Current. -- (from EV_CONTAINER) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed ensure -- from EV_PIXMAPABLE bridge_ok: (Result = Void and implementation.background_pixmap = Void) or (attached Result and then attached implementation.background_pixmap as l_pixmap and then Result.is_equal (l_pixmap)) collapse_node_pixmap: EV_PIXMAP -- Pixmap displayed within tree structures when a row with one or more -- subrows is expanded. Clicking the area occupied by this pixmap in Current -- collapses the row. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void column (a_column: INTEGER_32): EV_GRID_COLUMN -- Column at index 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): detachable EV_GRID_COLUMN -- Column at virtual x position a_virtual_x. require not_destroyed: not is_destroyed column_deselect_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_COLUMN] -- Actions to be performed when a column is deselected -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void column_select_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_COLUMN] -- Actions to be performed when a column is selected -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY] -- Agent used for customizing the Pick and Drop Target Menu of Current. -- (from EV_PICK_AND_DROPABLE) data: detachable ANY -- Arbitrary user data may be stored here. -- (from EV_ANY) default_identifier_name: STRING_32 -- Default name if no other name is set. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_key_processing_handler: detachable PREDICATE [EV_KEY] assign set_default_key_processing_handler -- Agent used to determine whether the default key processing should occur for Current. -- If agent returns True then default key processing continues as normal, False prevents -- default key processing from occurring. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.default_key_processing_handler deny_cursor: EV_POINTER_STYLE -- Result is cursor displayed when the screen pointer is over a -- target that does not accept `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE result_not_void: Result /= Void ensure then -- from EV_PICK_AND_DROPABLE cursor_valid: (attached implementation.deny_cursor implies Result = implementation.deny_cursor) or else Result = Default_pixmaps.No_cursor displayed_column (i: INTEGER_32): EV_GRID_COLUMN -- i-th displayed column. May not correspond -- to `column` if one or more columns have been --- hidden via `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: detachable FUNCTION [INTEGER_32, INTEGER_32, EV_GRID_ITEM] -- Function which computes the item that resides in a particular position of the -- grid while `is_content_partially_dynamic`. require not_is_destroyed: not is_destroyed expand_node_pixmap: EV_PIXMAP -- Pixmap displayed within tree structures when a row with one or more -- subrows is collapsed. Clicking the area occupied by this pixmap in Current -- expands the row. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void fill_background_actions: EV_LITE_ACTION_SEQUENCE [EV_DRAWABLE, INTEGER_32, INTEGER_32, INTEGER_32, INTEGER_32] -- Actions to be performed when part of the background area of the grid that is outside of the -- area filled by `row_count` and `column_count` needs to be redrawn. -- By default, the grid fills the area in its `background_color`. If one or more agents are -- contained in this action sequence, the grid is no longer responsible for drawing its background -- and the agents must redraw this area, otherwise graphical glitches may appear. -- The five pieces of event data passed are: -- drawable: EV_DRAWABLE The drawable into which you must draw the background. -- virtual_x: INTEGER The virtual x position of the area to be redrawn. -- virtual_y: INTEGER The virtual y position of the area to be redrawn. -- width: INTEGER The width of the area that must be redrawn. -- height: INTEGER The height of the area that must be redrawn. -- The upper left corner of the drawing must start at 0x0 in drawable with an area given by `width` -- and `height`. The virtual coordinates specify the position of the area in relation to the grid's -- virtual positiion which is essential if you wish to draw something such as a texture which must be -- matched based on its position. -- Note that `fill_background_actions` may be fired multiple times to fill the complete area of the -- background that is invalid. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES not_void: Result /= Void focused_selection_color: EV_COLOR -- Color used to show selection within items while focused. require not_is_destroyed: not is_destroyed ensure result_not_void: Result /= Void focused_selection_text_color: EV_COLOR -- Color used to for text of selected items while focused. require not_is_destroyed: not is_destroyed ensure result_not_void: Result /= Void foreground_color: EV_COLOR -- Color of foreground features like text. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed ensure -- from EV_COLORIZABLE bridge_ok: Result.is_equal (implementation.foreground_color) full_identifier_path: STRING_32 -- Full name of object by prepending path of parent -- Uses '.' as a separator. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_correct: parent = Void implies Result.is_equal (identifier_name) result_correct: attached parent as l_parent implies Result.is_equal (l_parent.full_identifier_path + ".".as_string_32 + identifier_name) generating_type: TYPE [detachable EV_GRID] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty cell_has (v: EV_WIDGET): BOOLEAN -- Does Current include v? -- (from EV_CELL) ensure -- from CONTAINER not_found_in_empty: Result implies not cell_is_empty cell_has_recursive (an_item: like cell_item): BOOLEAN -- Does structure include an_item or -- does any structure recursively included by structure, -- include an_item. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed header: EV_GRID_HEADER -- Header control used for resizing columns of Current. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void help_context: detachable FUNCTION [EV_HELP_CONTEXT] -- Agent that evaluates to help context sent to help engine when help is requested -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed ensure -- from EV_HELP_CONTEXTABLE bridge_ok: Result = implementation.help_context horizontal_scroll_bar: EV_HORIZONTAL_SCROLL_BAR -- Horizontal scrollbar used for scrolling Current. -- Use `is_horizontal_scroll_bar_show_requested` to find out if scrollbar will be shown if -- needed (i.e. when `virtual_width` is greater than `viewable_width`). require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void frozen id_object (an_id: INTEGER_32): detachable IDENTIFIED -- Object associated with an_id (void if no such object) -- (from IDENTIFIED) ensure -- from IDENTIFIED consistent: Result = Void or else Result.object_id = an_id identifier_name: STRING_32 -- Name of object -- If no specific name is set, `default_identifier_name` is used. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name) is_column_resize_immediate: BOOLEAN -- Is the user resizing of a column reflected immediately in Current? -- If True, the column width is updated continuosly and the state of `is_resizing_divider_enabled` -- is ignored with no divider displayed. -- If False, the column width is only updated upon completion of the resize. require not_destroyed: not is_destroyed is_content_partially_dynamic: BOOLEAN -- Is the content of Current partially dynamic? If True then -- whenever an item must be re-drawn and it is not already set within Current, -- then it is queried via execution of `dynamic_content_function`. The returned item is added -- to Current so the query only occurs once. require not_destroyed: not is_destroyed is_docking_enabled: BOOLEAN -- May Current be docked to? -- If True, Current will accept docking -- from a compatible EV_DOCKABLE_SOURCE. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET bridge_ok: Result = implementation.is_docking_enabled is_full_redraw_on_virtual_position_change_enabled: BOOLEAN -- Is complete client area invalidated as a result of virtual position changing? -- Note that enabling this causes a large performance penalty in redrawing during -- scrolling, but may be used to achieve effects not otherwise possible unless the -- entire client area is invalidated. require not_is_destroyed: not is_destroyed is_header_displayed: BOOLEAN -- Is the header displayed in Current. require not_destroyed: not is_destroyed is_horizontal_overscroll_enabled: BOOLEAN -- Does the virtual width of Current include the -- position of the final column plus the `viewable_width`. -- If True, this enables horizontal scrolling until the last column -- is at the very left of the viewable area. If False, scrolling -- may be performed until the last column is at the left of the viewable -- area. require not_destroyed: not is_destroyed is_horizontal_scrolling_per_item: BOOLEAN -- Is horizontal scrolling performed on a per-item basis? -- If True, each change of the horizontal scroll bar increments the horizontal -- offset by the current column width. -- If False, the scrolling is smooth on a per-pixel basis. require not_destroyed: not is_destroyed is_locked: BOOLEAN -- Are all graphical updates to Current suppressed until -- `unlock_update` is called. require not_is_destroyed: not is_destroyed is_resizing_divider_enabled: BOOLEAN -- Is a vertical divider displayed during column resizing? -- Note that if `is_column_resize_immediate` is True, Result -- is ignored by Current and no resizing divider is displayed. require not_destroyed: not is_destroyed is_resizing_divider_solid: BOOLEAN -- Is resizing divider displayed during column resizing drawn as a solid line? -- If False, a dashed line style is used. require not_destroyed: not is_destroyed is_row_height_fixed: BOOLEAN -- Must all rows in Current have the same height? require not_destroyed: not is_destroyed is_vertical_overscroll_enabled: BOOLEAN -- Does the virtual height of Current include the -- position of the final row plus the `viewable_height`. -- If True, this enables vertical scrolling until the last row -- is at the very top of the viewable area. If False, scrolling -- may be performed until the last row is at the bottom of the viewable -- area. require not_destroyed: not is_destroyed is_vertical_scrolling_per_item: BOOLEAN -- Is vertical scrolling performed on a per-item basis? -- If True, each change of the vertical scroll bar increments the vertical -- offset by the current row height. -- If False, the scrolling is smooth on a per-pixel basis. require not_destroyed: not is_destroyed cell_item: EV_WIDGET -- Current item. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed readable: Readable ensure -- from EV_CONTAINER bridge_ok: Result = implementation.interface_item item (a_column: INTEGER_32; a_row: INTEGER_32): detachable EV_GRID_ITEM -- Cell at a_row and a_column position, Void if none. 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: detachable FUNCTION [EV_GRID_ITEM, EV_POINTER_STYLE] -- Function used to retrieve the PND accept cursor for a particular item. -- Called directly after `item_pebble_function` has executed. require not_destroyed: not is_destroyed item_activate_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_ITEM, EV_POPUP_WINDOW] -- Actions to be performed to override the default activate setup of an item, see {EV_GRID_EDITABLE_ITEM}.activate_action. -- Useful for repositioning popup_window, which will then be shown automatically by the grid. -- Arguments of TUPLE (with names for clarity): -- -- activate_item: EV_GRID_ITEM -- The item that is currently activated. -- popup_window: EV_POPUP_WINDOW -- The popup window used to interactively edit activate_item, window has already been sized and positioned. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void item_at_virtual_position (a_virtual_x, a_virtual_y: INTEGER_32): detachable EV_GRID_ITEM -- Cell at virtual position a_virtual_x, a_virtual_y or -- Void if none. require not_destroyed: not is_destroyed item_deactivate_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item has been deactivated. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void item_deny_cursor_function: detachable FUNCTION [EV_GRID_ITEM, EV_POINTER_STYLE] -- Function used to retrieve the PND deny cursor for a particular item. -- Called directly after `item_pebble_function` has executed. require not_destroyed: not is_destroyed item_deselect_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item is deselected. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void item_drop_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_ITEM, ANY] -- Actions to be performed when a pebble is dropped on an item. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void item_pebble_function: detachable FUNCTION [detachable EV_GRID_ITEM, detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- It will be called once each time a pick on the item area of the grid occurs, the result -- will be assigned to `pebble` for the duration of transport. -- When a pick occurs on an item, the item itself is passed. -- If a pick occurs and no item is present, then Void is passed. require not_destroyed: not is_destroyed item_select_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item is selected. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void item_veto_pebble_function: detachable FUNCTION [EV_GRID_ITEM, ANY, BOOLEAN] -- Function used to determine whether dropping is allowed on a particular item. -- When called during PND transport, the grid item currently under the pebble -- and the pebble itself are passed to the function. A return value of True means -- that the pebble is allowed to be dropped onto the item, a return value of False -- disallows any PND transport. require not_destroyed: not is_destroyed locked_columns: ARRAYED_LIST [EV_GRID_COLUMN] -- All columns locked within Current in order of locking. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void locked_rows: ARRAYED_LIST [EV_GRID_ROW] -- All rows locked within Current in order of locking. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void maximum_virtual_x_position: INTEGER_32 -- Maximum permitted virtual x position based on current dimensions and properties. -- Properties that affect this value are `is_vertical_scrolling_per_item` and -- `is_vertical_overscroll_enabled`. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 maximum_virtual_y_position: INTEGER_32 -- Maximum permitted virtual y position based on current dimensions and properties. -- Properties that affect this value are `is_horizontal_scrolling_per_item` and -- `is_horizontal_overscroll_enabled`. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 non_focused_selection_color: EV_COLOR -- Color used to show selection within items while not focused. require not_is_destroyed: not is_destroyed ensure result_not_void: Result /= Void non_focused_selection_text_color: EV_COLOR -- Color used for text of selected items while not focused. require not_is_destroyed: not is_destroyed ensure result_not_void: Result /= Void frozen object_id: INTEGER_32 -- Unique for current object in any given session -- (from IDENTIFIED) ensure -- from IDENTIFIED valid_id: Result > 0 implies id_object (Result) = Current parent: detachable EV_CONTAINER -- Contains Current. -- (from EV_WIDGET) require -- from EV_IDENTIFIABLE not_destroyed: not is_destroyed ensure -- from EV_IDENTIFIABLE correct: has_parent implies Result /= Void correct: not has_parent implies Result = Void ensure then -- from EV_WIDGET bridge_ok: Result = implementation.parent pebble: detachable ANY -- Data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble pebble_function: detachable FUNCTION [detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_function pebble_positioning_enabled: BOOLEAN -- If True then pick and drop start coordinates are -- `pebble_x_position`, `pebble_y_position`. -- If False then pick and drop start coordinates are -- the pointer coordinates. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_positioning_enabled pebble_x_position: INTEGER_32 -- Initial x position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_x_position pebble_y_position: INTEGER_32 -- Initial y position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_y_position pointer_button_press_item_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32, INTEGER_32, detachable EV_GRID_ITEM] -- Actions to be performed when a pointer press event is received by a grid. -- Arguments (with names for clarity): -- -- x_pos: INTEGER -- The x position of the press in grid virtual coordinates. -- y_pos: INTEGER -- The y position of the press in grid virtual coordinates. -- a_button: INTEGER -- The index of the pressed button. -- item: EV_GRID_ITEM -- If the press occurred above an item, this is the pointed item, otherwise argument is set to Void. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_button_release_item_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32, INTEGER_32, detachable EV_GRID_ITEM] -- Actions to be performed when a pointer release event is received by a grid. -- Arguments (with names for clarity): -- -- x_pos: INTEGER -- The x position of the release in grid virtual coordinates. -- y_pos: INTEGER -- The y position of the release in grid virtual coordinates. -- a_button: INTEGER -- The index of the released button. -- item: EV_GRID_ITEM -- If the release occurred above an item, this is the pointed item, otherwise argument is set to Void. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_double_press_item_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32, INTEGER_32, detachable EV_GRID_ITEM] -- Actions to be performed when a pointer double press event is received by a grid. -- Arguments (with names for clarity): -- -- x_pos: INTEGER -- The x position of the double press in grid virtual coordinates. -- y_pos: INTEGER -- The y position of the double press in grid virtual coordinates. -- a_button: INTEGER -- The index of the pressed button. -- item: EV_GRID_ITEM -- If the double press occurred above an item, this is the pointed item, otherwise argument is set to Void. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_enter_item_actions: EV_LITE_ACTION_SEQUENCE [BOOLEAN, detachable EV_GRID_ITEM] -- Actions to be performed when a pointer enter event is received by a grid or grid item -- Arguments (with names for clarity): -- -- on_grid: BOOLEAN -- Did the enter event occur for the grid? -- item: EV_GRID_ITEM -- If the enter event occurred for an item, this is the item. -- -- Note that on_grid may be set to True and `item` may be non-Void -- in the case where the pointer enters a grid at a location where there -- is an item contained. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_leave_item_actions: EV_LITE_ACTION_SEQUENCE [BOOLEAN, detachable EV_GRID_ITEM] -- Actions to be performed when a pointer leave event is received by a grid or grid item -- Arguments (with names for clarity): -- -- on_grid: BOOLEAN -- Did the leave event occur for the grid? -- item: EV_GRID_ITEM -- If the leave event occurred for an item, this is the item. -- -- Note that on_grid may be set to True and `item` may be non-Void -- in the case where the pointer leaves a grid from a location where there -- was an item contained. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_motion_item_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32, detachable EV_GRID_ITEM] -- Actions to be performed when a screen pointer moves over a grid. -- Arguments (with names for clarity): -- -- x_pos: INTEGER -- The x position of the motion in grid virtual coordinates. -- y_pos: INTEGER -- The y position of the motion in grid virtual coordinates. -- item: EV_GRID_ITEM -- If the motion occurred above an item, this is the pointed item, otherwise argument is set to Void. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void pointer_position: EV_COORDINATE -- Position of the screen pointer relative to Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_show_requested: is_show_requested pointer_style: EV_POINTER_STYLE -- Cursor displayed when pointer is over this widget. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed post_draw_overlay_actions: EV_LITE_ACTION_SEQUENCE [EV_DRAWABLE, detachable EV_GRID_ITEM, INTEGER_32, INTEGER_32] -- Actions to be performed after an item cell in Current has been drawn. The four pieces of event data are: -- drawable: EV_DRAWABLE The drawable into which you may draw to overlay onto the already drawn item. -- grid_item: EV_GRID_ITEM The item which has just been drawn, may be Void in the case that an -- item cell is being drawn which does not contain an item. -- a_column_index: INTEGER The column index of the grid cell that has just been drawn. -- a_row_index: INTEGER The row index of the grid cell that has just been drawn. -- This is useful for drawing additional border styles or other such effects. The upper left corner -- of the item cell starts at coordinates 0x0 in the passed drawable. All drawing Performed -- in the drawable is clipped to `width` of the column at a_column_index and `height` of row at a_row_index. -- Note that the upper left corner of drawable corresponds to the upper left corner of the item -- cell and not the actual items horizontal position within the cell which may be greater than 0 if -- the item is within a tree structure. Use horizontal_indent of the item to determine this. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES not_void: Result /= Void pre_draw_overlay_actions: EV_LITE_ACTION_SEQUENCE [EV_DRAWABLE, detachable EV_GRID_ITEM, INTEGER_32, INTEGER_32] -- Actions to be performed before the features of an item cell in Current have been drawn but after the background of -- the cell has been drawn. The four pieces of event data are: -- drawable: EV_DRAWABLE The drawable into which you may draw to overlay onto the already drawn background. -- grid_item: EV_GRID_ITEM The item which has just been drawn, may be Void in the case that an -- item cell is being drawn which does not contain an item. -- a_column_index: INTEGER The column index of the grid cell that has just been drawn. -- a_row_index: INTEGER The row index of the grid cell that has just been drawn. -- This is useful for drawing additional border styles or other such effects. The upper left corner -- of the item cell starts at coordinates 0x0 in the passed drawable. All drawing Performed -- in the drawable is clipped to `width` of the column at a_column_index and `height` of row at a_row_index. -- Note that the upper left corner of drawable corresponds to the upper left corner of the item -- cell and not the actual items horizontal position within the cell which may be greater than 0 if -- the item is within a tree structure. Use horizontal_indent of the item to determine this. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES not_void: Result /= Void real_target: detachable EV_DOCKABLE_TARGET -- Result is target used during a dockable transport if -- mouse pointer is above Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.real_target remove_selection -- Ensure that `selected_items`, `selected_rows` and `selected_columns` are empty. 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 -- Row at index 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): detachable EV_GRID_ROW -- Row at virtual y position a_virtual_y. require not_destroyed: not is_destroyed row_collapse_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is collapsed. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void row_deselect_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is deselected. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void row_expand_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is expanded. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void row_height: INTEGER_32 -- Height of all rows within Current. Only has an effect on Current -- while `is_row_height_fixed`, otherwise the individual height of each -- row is used directly. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 row_select_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is selected. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void selected_columns: ARRAYED_LIST [EV_GRID_COLUMN] -- All columns selected in Current. -- Returned list is unsorted so no particular ordering is guaranteed. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void selected_items: ARRAYED_LIST [EV_GRID_ITEM] -- All items selected in Current. -- Returned list is unsorted so no particular ordering is guaranteed. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void selected_rows: ARRAYED_LIST [EV_GRID_ROW] -- All rows selected in Current. -- Returned list is unsorted so no particular ordering is guaranteed. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void separator_color: EV_COLOR -- Color used to display column and row separators. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void subrow_indent: INTEGER_32 -- Number of pixels horizontally by which each subrow is indented -- from its parent_row. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 target_data_function: detachable FUNCTION [like pebble, EV_PND_TARGET_DATA] -- Function for computing target meta data based on source pebble. -- Primarily used for Pick and Drop target menu. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) note option: stable target_name: detachable READABLE_STRING_GENERAL -- Optional textual name describing Current pick and drop hole. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) note option: stable tooltip: STRING_32 -- Tooltip displayed on Current. -- If Result is empty then no tooltip displayed. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed ensure -- from EV_TOOLTIPABLE bridge_ok: is_bridge_ok (Result) not_void: Result /= Void cloned: is_cloned (Result) vertical_scroll_bar: EV_VERTICAL_SCROLL_BAR -- Vertical scrollbar used for scrolling Current. -- Use `is_vertical_scroll_bar_show_requested` to find out if scrollbar will be shown if -- needed (i.e. when `virtual_height` is greater than `viewable_height`). require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void veto_dock_function: detachable FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN] -- Function to determine whether current dock is allowed. -- If Result is True, dock will be disallowed. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET bridge_ok: Result = implementation.veto_dock_function viewable_height: INTEGER_32 -- Height of Current available to view displayed items. Does -- not include width of any displayed scroll bars and/or header if shown. require not_destroyed: not is_destroyed ensure viewable_height_valid: is_displayed implies viewable_height >= 0 and viewable_height <= height viewable_width: INTEGER_32 -- Width of Current available to view displayed items. Does -- not include width of any displayed scroll bars. require not_destroyed: not is_destroyed ensure viewable_width_valid: is_displayed implies viewable_width >= 0 and viewable_width <= width viewable_x_offset: INTEGER_32 -- Horizontal distance in pixels from the left edge of Current to -- the left edge of the viewable area (defined by `viewable_width`, `viewable_height`) -- in which all content is displayed. require not_destroyed: not is_destroyed ensure viewable_x_offset_valid: Result >= 0 and Result <= width viewable_y_offset: INTEGER_32 -- Vertical distance in pixels from the top edge of Current to -- the top edge of the viewable area (defined by `viewable_width`, `viewable_height`) -- in which all content is displayed. require not_destroyed: not is_destroyed ensure viewable_y_offset_valid: Result >= 0 and Result <= height virtual_height: INTEGER_32 -- Height of virtual area in pixels. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 virtual_position_changed_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32] -- Actions to be performed upon next idle after `virtual_x_position` or `virtual_y_position` changed in grid. -- Arguments (with names for clarity) -- -- a_virtual_x_position: INTEGER -- New `virtual_x_position` of grid. -- a_virtual_y_position: INTEGER -- New `virtual_y_position` of grid. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void virtual_size_changed_actions: EV_LITE_ACTION_SEQUENCE [INTEGER_32, INTEGER_32] -- Actions to be performed upon next idle after `virtual_width` or `virtual_height` changed in grid. -- Arguments (with names for clarity) -- -- a_virtual_width: INTEGER -- New `virtual_width` of grid. -- a_virtual_height: INTEGER -- New `virtual_height` of grid. -- (from EV_GRID_ACTION_SEQUENCES) ensure -- from EV_GRID_ACTION_SEQUENCES result_not_void: Result /= Void virtual_width: INTEGER_32 -- Width of virtual area in pixels. require not_destroyed: not is_destroyed ensure result_non_negative: Result >= 0 virtual_x_position: INTEGER_32 -- Horizontal offset of viewable area in relation to the left edge of -- the virtual area in pixels. require not_destroyed: not is_destroyed ensure valid_result: Result >= 0 and Result <= maximum_virtual_x_position virtual_y_position: INTEGER_32 -- Vertical offset of viewable area in relation to the top edge of -- the virtual area in pixels. require not_destroyed: not is_destroyed ensure valid_result: Result >= 0 and Result <= maximum_virtual_y_position feature -- Measurement cell_client_height: INTEGER_32 -- Height of the area available to children in pixels. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER bridge_ok: Result = implementation.client_height cell_client_width: INTEGER_32 -- Width of the area available to children in pixels. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER bridge_ok: Result = implementation.client_width dpi: NATURAL_32 -- Window dpi -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED positive_or_zero: Result >= 0 height: INTEGER_32 -- Vertical size in pixels. -- Same as `minimum_height` when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.height minimum_height: INTEGER_32 -- Lower bound on `height` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_height positive_or_zero: Result >= 0 minimum_width: INTEGER_32 -- Lower bound on `width` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_width positive_or_zero: Result >= 0 screen_x: INTEGER_32 -- Horizontal offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_x screen_y: INTEGER_32 -- Vertical offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_y width: INTEGER_32 -- Horizontal size in pixels. -- Same as `minimum_width` when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.width x_position: INTEGER_32 -- Horizontal offset relative to parent `x_position` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.x_position y_position: INTEGER_32 -- Vertical offset relative to parent `y_position` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.y_position feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal alias "≡≡≡" (other: EV_GRID): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) is_equal (other: EV_GRID): BOOLEAN -- Is other attached to an object considered -- equal to current object? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) frozen standard_is_equal alias "≜" (other: EV_GRID): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report are_columns_drawn_above_rows: BOOLEAN -- For drawing purposes, are columns drawn above rows? -- If True, for all cells within Current whose `column` and `row` have non-Void -- foreground or background colors, the column colors are given priority. -- If False, the colors of the row are given priority. require not_destroyed: not is_destroyed column_displayed (a_column: INTEGER_32): BOOLEAN -- May column a_column be displayed when Current is? -- Will return False if `hide` has been called on column a_column. -- A value of True does not signify that column a_column is visible on screen at that particular time. require not_destroyed: not is_destroyed a_column_within_bounds: a_column > 0 and a_column <= column_count conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void cell_count: INTEGER_32 -- Number of items in Current. -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure then -- from EV_CELL valid_result: Result = 0 or Result = 1 debug_output: STRING_32 -- String that should be displayed in debugger to represent Current. -- (from EV_IDENTIFIABLE) ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void depth_in_tree (a_row_index: INTEGER_32): INTEGER_32 -- Depth in tree for a_row require valid_index: 0 < a_row_index and a_row_index <= row_count cell_extendible: BOOLEAN -- Is there no element? -- Was declared in {EV_CELL} as synonym of is_empty. -- (from EV_CELL) find_next_item (a_row_index, a_column_index: INTEGER_32; look_left, a_is_tab_navigatable: BOOLEAN): detachable EV_GRID_ITEM -- Find the next item horizontally in grid_row starting at index starting_index, if 'look_left' then the the item to the left/up is found, else it looks right/down. -- If a_is_tab_navigatable then Result must have 'is_tab_navigatable' set. -- Result is Void if no item is found. require a_row_index_valid: a_row_index > 0 and then a_row_index <= row_count a_column_index_valid: a_column_index > 0 and then a_column_index <= column_count first_visible_column: detachable EV_GRID_COLUMN -- First column visible in Current or Void if `column_count` = 0 -- If `is_horizontal_scrolling_per_item`, the first visible column may be only partially visible. 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: detachable EV_GRID_ROW -- First row visible in Current or Void if `visible_row_count` = 0 -- If `is_vertical_scrolling_per_item`, the first visible row may be only partially visible. require not_destroyed: not is_destroyed is_displayed: is_displayed ensure has_rows_implies_result_not_void: visible_row_count > 0 implies Result /= Void no_rows_implies_result_void: visible_row_count = 0 implies Result = Void cell_full: BOOLEAN -- Is structure filled to capacity? -- (from EV_CELL) has_capture: BOOLEAN -- Does widget have capture? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_capture has_focus: BOOLEAN -- Does widget have the keyboard focus? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_focus has_identifier_name_set: BOOLEAN -- Is a specific identifier name set? -- (from EV_IDENTIFIABLE) has_parent: BOOLEAN -- Does identifiable has a parent? -- (from EV_IDENTIFIABLE) has_selected_column: BOOLEAN -- Has selected column? require not_destroyed: not is_destroyed ensure result_implies_selected_columns_not_empty: Result implies not selected_columns.is_empty has_selected_item: BOOLEAN -- Has selected items? require not_destroyed: not is_destroyed ensure result_implies_selected_items_not_empty: Result implies not selected_items.is_empty has_selected_row: BOOLEAN -- Has selected row? require not_destroyed: not is_destroyed ensure result_implies_selected_rows_not_empty: Result implies not selected_rows.is_empty frozen id_freed: BOOLEAN -- Has Current been removed from the table? -- (from IDENTIFIED) is_displayed: BOOLEAN -- Is Current visible on the screen? -- True when show requested and parent displayed. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.is_displayed is_dockable: BOOLEAN -- Is Current dockable? -- If True, then Current may be dragged -- from its current parent. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_dockable cell_is_empty: BOOLEAN -- Is there no element? -- Was declared in {EV_CELL} as synonym of extendible. -- (from EV_CELL) is_external_docking_enabled: BOOLEAN -- Is Current able to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport? -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_enabled is_external_docking_relative: BOOLEAN -- Will dockable dialog displayed when Current is docked externally -- be displayed relative to parent window of Current? -- Otherwise displayed as a standard window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_relative cell_is_inserted (v: EV_WIDGET): BOOLEAN -- Has v been inserted by the most recent insertion? -- (By default, the value returned is equivalent to calling -- has (v). However, descendants might be able to provide more -- efficient implementations.) -- (from COLLECTION) is_item_tab_navigation_enabled: BOOLEAN -- Is the tabbing mode for Current set so that keyboard tabbing moves to/from 'has_default_activation' grid items? is_multiple_item_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select an item, with multiple -- item selection permitted via the use of Ctrl and Shift keys? require not_destroyed: not is_destroyed is_multiple_row_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select the whole row, with multiple -- row selection permitted via the use of Ctrl and Shift keys? require not_destroyed: not is_destroyed is_selection_keyboard_handling_enabled: BOOLEAN -- May items be selected via the keyboard? require not_destroyed: not is_destroyed is_selection_on_click_enabled: BOOLEAN -- Will an item be selected if clicked upon? require not_destroyed: not is_destroyed is_selection_on_single_button_click_enabled: BOOLEAN -- Will an item be selected if clicked upon via mouse button 1 only? require not_destroyed: not is_destroyed is_sensitive: BOOLEAN -- Is object sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE bridge_ok: Result = implementation.user_is_sensitive is_show_requested: BOOLEAN -- Will Current be displayed when its parent is? -- See also `is_displayed`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.is_show_requested is_single_item_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select an item, unselecting -- any previously selected items? require not_destroyed: not is_destroyed is_single_row_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select the whole row, unselecting -- any previously rows? require not_destroyed: not is_destroyed is_tree_enabled: BOOLEAN -- Is tree functionality enabled? -- Must be True to perform any tree structure functions on Current. -- Use `enable_tree` and `disable_tree` to set this state. require not_destroyed: not is_destroyed last_visible_column: detachable EV_GRID_COLUMN -- Index of last column visible in Current or 0 if `column_count` = 0. -- The last visible column may be only partially visible. 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: detachable EV_GRID_ROW -- Last row visible in Current or Void if `visible_row_count` = 0 -- The last visible row may be only partially visible. require not_destroyed: not is_destroyed is_displayed: is_displayed ensure has_rows_implies_result_not_void: visible_row_count > 0 implies Result /= Void no_rows_implies_result_void: visible_row_count = 0 implies Result = Void cell_merged_radio_button_groups: detachable ARRAYED_LIST [EV_CONTAINER] -- Result is all other radio button groups -- merged with Current. Void if no other containers -- are merged. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER not_is_empty: Result /= Void implies not Result.is_empty mode_is_configurable_target_menu: BOOLEAN -- Is the user interface mode a configurable pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_configurable_target_menu mode_is_drag_and_drop: BOOLEAN -- Is the user interface mode drag and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_drag_and_drop mode_is_pick_and_drop: BOOLEAN -- Is the user interface mode pick and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_pick_and_drop mode_is_target_menu: BOOLEAN -- Is the user interface mode a pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_target_menu object_comparison: BOOLEAN -- Must search operations use `equal` rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) Prunable: BOOLEAN = False -- May items be removed? Readable: BOOLEAN = False -- Is there a current item that may be accessed? real_source: detachable EV_DOCKABLE_SOURCE -- Result is source to be dragged -- when a docking drag occurs on Current. -- If Void, Current is dragged. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.real_source same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) tree_node_connector_color: EV_COLOR -- Color of connectors drawn between tree nodes within Current. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void viewable_row_indexes: ARRAYED_LIST [INTEGER_32] -- Indexes of all rows that are currently viewable in the grid in its present state. -- For example, if the first node is a non expanded tree that has 10 subrows, the contents -- would be 1, 11, 12, 13, 14, ... -- This list only returns valid values if variable row heights, tree functionality or -- hidden nodes are enabled in the grid, otherwise the returned list is empty. require not_destroyed: not is_destroyed ensure result_not_void: Result /= Void visible_column_indexes: ARRAYED_LIST [INTEGER_32] -- All columns that are currently visible in Current. -- Result may not be contiguous if one or more columns are hidden. require not_destroyed: not is_destroyed is_displayed: is_displayed ensure result_not_void: Result /= Void visible_row_indexes: ARRAYED_LIST [INTEGER_32] -- Indexes of all rows that are currently visible in Current. -- Result may not be contiguous if `is_tree_enabled` and one or more of the -- visible rows have subrows and are not expanded. require not_destroyed: not is_destroyed is_displayed: is_displayed ensure result_not_void: Result /= Void Writable: BOOLEAN = False -- Is there a current item that may be modified? feature -- Status setting center_pointer -- Position screen pointer over center of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed compare_objects -- Ensure that future search operations will use `equal` -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than `equal` for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison disable_always_selected -- Allow the user to completely remove the selection from Current via clicking on an item, -- clicking on a Void area or by Ctrl clicking the selected item itself. require not_destroyed: not is_destroyed ensure not_is_item_always_selected_enabled: not is_always_selected disable_capture -- Disable grab of all user input events. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET not_has_capture: not has_capture disable_column_resize_immediate -- Ensure `is_column_resize_immediate` is False. require not_destroyed: not is_destroyed ensure not_is_column_resize_immediate: not is_column_resize_immediate disable_column_separators -- Ensure `are_column_separators_enabled` is False. require not_destroyed: not is_destroyed ensure column_separators_disabled: not are_column_separators_enabled disable_columns_drawn_above_rows -- Ensure `are_columns_drawn_above_rows` is False. require not_destroyed: not is_destroyed ensure columns_drawn_below_rows: not are_columns_drawn_above_rows disable_dockable -- Ensure Current is not dockable. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE not_is_dockable: not is_dockable disable_docking -- Ensure `is_docking_enabled` is False. -- Current will not accept docking. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET not_dockable: not is_docking_enabled disable_dynamic_content -- Ensure contents of Current are not dynamic and are no longer retrieved as such. require not_destroyed: not is_destroyed ensure content_not_dynamic: not is_content_partially_dynamic disable_external_docking -- Assign False to `is_external_docking_enabled`. -- Forbid Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE not_externally_dockable: not is_external_docking_enabled disable_external_docking_relative -- Assign False to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed as a standard window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE external_docking_not_relative: not is_external_docking_relative disable_focus_on_press -- Disable focus handling when mouse button is pressed on grid excluding header and scrollbars. require not_destroyed: not is_destroyed disable_full_redraw_on_virtual_position_change -- Ensure `is_full_redraw_on_virtual_position_change_enabled` is 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 -- Ensure `is_horizontal_overscroll_enabled` is False. require not_destroyed: not is_destroyed ensure not_is_horizontal_overscroll_enabled: not is_horizontal_overscroll_enabled disable_horizontal_scrolling_per_item -- Ensure horizontal scrolling is performed on a per-pixel basis. require not_destroyed: not is_destroyed ensure horizontal_scrolling_performed_per_pixel: not is_horizontal_scrolling_per_item disable_item_tab_navigation -- Disable tabbed item navigation so that tabbing loses focus from the grid by default. require not_destroyed: not is_destroyed ensure tabbed_item_navigation_disabled: not is_item_tab_navigation_enabled disable_pebble_positioning -- Assign False to `pebble_positioning_enabled`. -- The pick and drop will start at the pointer position. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_positioning_updated: not pebble_positioning_enabled disable_resizing_divider -- Ensure no vertical divider is displayed during column resizing. require not_destroyed: not is_destroyed ensure resizing_divider_disabled: not is_resizing_divider_enabled disable_row_height_fixed -- Permit rows to have varying heights. 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 -- Ensure `are_row_separators_enabled` is False. require not_destroyed: not is_destroyed ensure row_separators_disabled: not are_row_separators_enabled disable_selection_key_handling -- Disable selection handling of items via the keyboard. require not_destroyed: not is_destroyed ensure selection_key_handling_disabled: not is_selection_keyboard_handling_enabled disable_selection_on_click -- Disable selection handling when items are clicked upon. 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 -- Make object non-sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE is_unsensitive: not is_sensitive disable_solid_resizing_divider -- Ensure resizing divider displayed during column resizing -- is displayed as a dashed line. require not_destroyed: not is_destroyed ensure dashed_resizing_divider: not is_resizing_divider_solid disable_tree -- Disable tree functionality for Current. -- All subrows of rows contained are unparented, -- which flattens the tree structure. require not_destroyed: not is_destroyed ensure tree_disabled: not is_tree_enabled disable_vertical_overscroll -- Ensure `is_vertical_overscroll_enabled` is 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 -- Ensure vertical scrolling is performed on a per-pixel basis. 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 -- Ensure that the user may not completely remove the selection from Current. require not_destroyed: not is_destroyed ensure item_is_always_selected_enabled: is_always_selected enable_capture -- Grab all user input events (mouse and keyboard). -- `disable_capture` must be called to resume normal input handling. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_displayed: is_displayed ensure -- from EV_WIDGET has_capture: has_capture enable_column_resize_immediate -- Ensure `is_column_resize_immediate` is True. require not_destroyed: not is_destroyed ensure is_column_resize_immediate: is_column_resize_immediate enable_column_separators -- Ensure `are_column_separators_enabled` is True. require not_destroyed: not is_destroyed ensure column_separators_enabled: are_column_separators_enabled enable_columns_drawn_above_rows -- Ensure `are_columns_drawn_above_rows` is True. require not_destroyed: not is_destroyed ensure columns_drawn_above_rows: are_columns_drawn_above_rows enable_dockable -- Ensure Current is dockable. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE is_dockable: is_dockable enable_docking -- Ensure `is_docking_enabled` is True. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET is_dockable: is_docking_enabled enable_external_docking -- Assign True to `is_external_docking_enabled`. -- Allows Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE is_externally_dockable: is_external_docking_enabled enable_external_docking_relative -- Assign True to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed relative to the top level window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE external_docking_not_relative: is_external_docking_relative enable_focus_on_press -- Enable focus handling when mouse button is pressed on grid excluding header and scrollbars. require not_destroyed: not is_destroyed enable_full_redraw_on_virtual_position_change -- Ensure `is_full_redraw_on_virtual_position_change_enabled` is 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 -- Ensure `is_horizontal_overscroll_enabled` is True. require not_destroyed: not is_destroyed ensure is_horizontal_overscroll_enabled: is_horizontal_overscroll_enabled enable_horizontal_scrolling_per_item -- Ensure horizontal scrolling is performed on a per-item basis. require not_destroyed: not is_destroyed ensure horizontal_scrolling_performed_per_item: is_horizontal_scrolling_per_item enable_item_tab_navigation -- Allow keyboard tab navigation to occur within current for items that return True for 'has_default_activation'. -- Tabbing in to the grid from a previous widget will select the first item. -- Shift/Tabbing in to the grid will select the most bottom/right default activable grid item. require not_destroyed: not is_destroyed ensure tabbed_item_navigation_enabled: is_item_tab_navigation_enabled enable_multiple_item_selection -- Allow the user to select more than one item via clicking or navigating using the keyboard arrow keys. -- Multiple items may be selected via Ctrl and Shift keys. require not_destroyed: not is_destroyed ensure multiple_item_selection_enabled: is_multiple_item_selection_enabled enable_multiple_row_selection -- Allow the user to select more than one row via clicking or navigating using the keyboard arrow keys. -- Multiple rows may be selected via Ctrl and Shift keys. require not_destroyed: not is_destroyed ensure multiple_row_selection_enabled: is_multiple_row_selection_enabled enable_partial_dynamic_content -- Ensure contents of Current must be retrieved when required via execution of -- `dynamic_content_function` only if the item is not already set -- in 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 -- Assign True to `pebble_positioning_enabled`. -- Use `pebble_x_position` and `pebble_y_position` as the initial coordinates -- for the pick and drop in pixels relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_positioning_updated: pebble_positioning_enabled enable_resizing_divider -- Ensure a vertical divider is displayed during column resizing. require not_destroyed: not is_destroyed ensure resizing_divider_enabled: is_resizing_divider_enabled enable_row_height_fixed -- Ensure all rows have the same height. require not_destroyed: not is_destroyed ensure row_height_fixed: is_row_height_fixed enable_row_separators -- Ensure `are_row_separators_enabled` is True. require not_destroyed: not is_destroyed ensure row_separators_enabled: are_row_separators_enabled enable_selection_key_handling -- Enable selection handling of items via the keyboard. require not_destroyed: not is_destroyed ensure selection_key_handling_enabled: is_selection_keyboard_handling_enabled enable_selection_on_click -- Enable selection handling of items when clicked upon via mouse button. 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 -- Enable selection handling of items when clicked upon via mouse button 1. -- This is useful when implementing Contextual Menus where the selection may need -- to remain unchanged when using mouse button 3 to handle the menu. 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 -- Make object sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE is_sensitive: (parent = Void or parent_is_sensitive) implies is_sensitive enable_single_item_selection -- Allow the user to select a single item via clicking or navigating using the keyboard arrow keys. require not_destroyed: not is_destroyed ensure single_item_selection_enabled: is_single_item_selection_enabled enable_single_row_selection -- Allow the user to select a single row via clicking or navigating using the keyboard arrow keys. require not_destroyed: not is_destroyed ensure single_row_selection_enabled: is_single_row_selection_enabled enable_solid_resizing_divider -- Ensure resizing divider displayed during column resizing -- is displayed as a solid line. require not_destroyed: not is_destroyed ensure solid_resizing_divider: is_resizing_divider_solid enable_tree -- Enable tree functionality for Current. require not_destroyed: not is_destroyed ensure tree_enabled: is_tree_enabled enable_vertical_overscroll -- Ensure `is_vertical_overscroll_enabled` is True. require not_destroyed: not is_destroyed ensure is_vertical_overscroll_enabled: is_vertical_overscroll_enabled enable_vertical_scrolling_per_item -- Ensure vertical scrolling is performed on a per-item basis. require not_destroyed: not is_destroyed ensure vertical_scrolling_performed_per_item: is_vertical_scrolling_per_item hide -- Request that Current not be displayed even when its parent is. -- If successful, make `is_show_requested` False. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed hide_column (a_column: INTEGER_32) -- Ensure column a_column is not visible in 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 -- Ensure header is hidden. require not_destroyed: not is_destroyed ensure header_not_displayed: not is_header_displayed hide_horizontal_scroll_bar -- Ensure no horizontal scroll bar is displayed in Current -- at any time. 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 -- Ensure no connectors are displayed between nodes of tree structure in Current. require not_destroyed: not is_destroyed ensure tree_node_connectors_hidden: not are_tree_node_connectors_shown hide_vertical_scroll_bar -- Ensure no vertical scroll bar is displayed in Current -- at any time. 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 -- May the user completely remove the selection from the grid. -- If True then the user of the grid may only deselect items by selecting other items. require not_destroyed: not is_destroyed is_horizontal_scroll_bar_show_requested: BOOLEAN -- Will a horizontal scroll bar be displayed in Current when -- `virtual_width` exceeds `viewable_width`? require not_is_destroyed: not is_destroyed is_vertical_scroll_bar_show_requested: BOOLEAN -- Will a vertical scroll bar be displayed in Current when -- `virtual_height` exceeds `viewable_height`? require not_is_destroyed: not is_destroyed lock_update -- Ensure `is_locked` is True, thereby preventing graphical -- updates until `unlock_update` is called. require not_is_destroyed: not is_destroyed ensure is_locked: is_locked cell_merge_radio_button_groups (other: EV_CONTAINER) -- Merge Current radio button group with that of other. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed other_not_void: other /= Void redraw -- Force Current to be re-drawn when next idle. require not_destroyed: not is_destroyed remove_default_key_processing_handler -- Ensure `default_key_processing_handler` is Void. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed remove_pebble -- Make `pebble` Void and `pebble_function` `Void, -- Removing transport. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_removed: pebble = Void and pebble_function = Void remove_real_source -- Ensure `real_source` is Void. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE real_source_void: real_source = Void remove_real_target -- Ensure `real_target` is Void. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET real_target_void: real_target = Void select_column (a_column: INTEGER_32) -- Ensure all items in a_column are selected. 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) -- Ensure all items in a_row are selected. 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: detachable like accept_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE accept_cursor_assigned: attached a_cursor as l_accept_cursor implies l_accept_cursor ~ accept_cursor set_actual_drop_target_agent (an_agent: like actual_drop_target_agent) -- Assign an_agent to `actual_drop_target_agent`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed an_agent_not_void: an_agent /= Void ensure -- from EV_WIDGET assigned: actual_drop_target_agent = an_agent set_column_count_to (a_column_count: INTEGER_32) -- Resize Current to have a_column_count columns. require not_destroyed: not is_destroyed a_column_count_positive: a_column_count >= 0 ensure column_count_set: column_count = a_column_count set_configurable_target_menu_handler (a_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY]) -- Set Configurable Target Menu Handler to a_handler. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_PICK_AND_DROPABLE configurable_target_menu_hander_assigned: configurable_target_menu_handler = a_handler set_configurable_target_menu_mode -- Set user interface mode to pop-up menu of targets. -- Target menu is configurable as the first option can be used to -- initiate a regular 'pick and drop' of the source pebble. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE target_menu_mode_set: mode_is_configurable_target_menu set_default_colors -- Set foreground and background color to their default values. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed set_default_key_processing_handler (a_handler: like default_key_processing_handler) -- Assign `default_key_processing_handler` to a_handler. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed set_deny_cursor (a_cursor: detachable like deny_cursor) -- Set a_cursor to be displayed when the screen pointer is not -- over a valid target. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE deny_cursor_assigned: attached a_cursor as l_deny_cursor implies l_deny_cursor ~ deny_cursor set_drag_and_drop_mode -- Set user interface mode to drag and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE drag_and_drop_set: mode_is_drag_and_drop set_dynamic_content_function (a_function: FUNCTION [INTEGER_32, INTEGER_32, EV_GRID_ITEM]) -- Function which computes the item that resides in a particular position of the -- grid while `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) -- Set a_row as the first row visible in Current as long -- as there are enough rows after a_row to fill the remainder of 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 -- Grab keyboard focus if `is_displayed`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_sensitive: is_sensitive set_focused_selection_color (a_color: EV_COLOR) -- Assign a_color to `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) -- Assign a_color to `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 [EV_GRID_ITEM, EV_POINTER_STYLE]) -- Assign a_function to `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 [EV_GRID_ITEM, EV_POINTER_STYLE]) -- Assign a_function to `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 [detachable EV_GRID_ITEM, detachable ANY]) -- Assign a_function to `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 [EV_GRID_ITEM, ANY, BOOLEAN]) -- Assign a_function to `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) -- Assign an_expand_node_pixmap to `expand_node_pixmap` and a_collapse_node_pixmap -- to `collapse_node_pixmap`. These pixmaps are used in rows containing subrows for -- expanding/collapsing the row. 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) -- Assign a_color to `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) -- Assign a_color to `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: ANY) -- Assign a_pebble to `pebble`. -- Overrides `set_pebble_function`. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_pebble_not_void: a_pebble /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_assigned: pebble = a_pebble set_pebble_function (a_function: FUNCTION [detachable ANY]) -- Set a_function to compute `pebble`. -- It will be called once each time a pick occurs, the result -- will be assigned to `pebble` for the duration of transport. -- When a pick occurs, the pick position in widget coordinates, -- <<x, y>> in pixels, is passed. -- To handle this data use a_function of type -- FUNCTION [ANY, TUPLE [INTEGER, INTEGER], ANY] and return the -- pebble as a function of x and y. -- Overrides `set_pebble`. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_function_not_void: a_function /= Void a_function_takes_two_integer_open_operands: a_function.valid_operands ([1, 1]) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_function_assigned: pebble_function = a_function set_pebble_position (a_x, a_y: INTEGER_32) -- Set the initial position for pick and drop -- Coordinates are in pixels and are relative to position of Current. -- Pebble_positioning_enabled must be True for the position to be used, -- use enable_pebble_positioning. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y set_pick_and_drop_mode -- Set user interface mode to pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pick_and_drop_set: mode_is_pick_and_drop set_real_source (dockable_source: EV_DOCKABLE_SOURCE) -- Assign dockable_source to `real_source`. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable dockable_source_not_void: dockable_source /= Void dockable_source_is_parent_recursive: source_has_current_recursive (dockable_source) ensure -- from EV_DOCKABLE_SOURCE real_source_assigned: real_source = dockable_source set_real_target (a_target: EV_DOCKABLE_TARGET) -- Assign a_target to `real_target`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed target_not_void: a_target /= Void ensure -- from EV_WIDGET assigned: real_target = a_target set_row_count_to (a_row_count: INTEGER_32) -- Resize Current to have a_row_count rows. 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) -- Set height of all rows within Current to `a_row_height -- If not `is_row_height_fixed` then use the height individually per row instead. require not_destroyed: not is_destroyed a_row_height_positive: a_row_height >= 1 ensure row_height_set: row_height = a_row_height set_separator_color (a_color: EV_COLOR) -- Set a_color as `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) -- Set `subrow_indent` to 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_data_function (a_function: FUNCTION [like pebble, EV_PND_TARGET_DATA]) -- Set a_function to compute target meta data based on transport source. -- Overrides any `target_name` set with `set_target_name`. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_function_not_void: a_function /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE target_data_function_assigned: target_data_function /= Void and then target_data_function.is_equal (a_function) set_target_menu_mode -- Set user interface mode to pop-up menu of targets. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE target_menu_mode_set: mode_is_target_menu set_target_name (a_name: READABLE_STRING_GENERAL) -- Assign a_name to `target_name`. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_name_not_void: a_name /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE target_name_assigned: attached target_name as l_target_name and then a_name /= l_target_name and then a_name.same_string (l_target_name) set_tree_node_connector_color (a_color: EV_COLOR) -- Set a_color as `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 [EV_DOCKABLE_SOURCE, BOOLEAN]) -- Assign a_function to `veto_dock_function`. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed a_function_not_void: a_function /= Void ensure -- from EV_DOCKABLE_TARGET veto_function_set: veto_dock_function = a_function set_virtual_position (virtual_x, virtual_y: INTEGER_32) -- Move viewable area of Current to virtual position 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 -- Request that Current be displayed when its parent is. -- True by default. -- If successful, make `is_show_requested` True. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed show_column (a_column: INTEGER_32) -- Ensure column a_column is visible in 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_configurable_target_menu (a_x, a_y: INTEGER_32) -- Show the configurable target menu at position a_x, a_y relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed mode_is_configurable_target_menu: mode_is_configurable_target_menu configurable_menu_handler_set: configurable_target_menu_handler /= Void show_header -- Ensure header displayed. require not_destroyed: not is_destroyed ensure header_displayed: is_header_displayed show_horizontal_scroll_bar -- Ensure a horizontal scroll bar is displayed in Current -- when required. Note that this does not force the horizontal -- scroll bar to be visible, simply ensures that when `virtual_width` -- is greater than `viewable_width`, the scroll bar is displayed. require not_is_destroyed: not is_destroyed ensure is_horizontal_scroll_bar_show_requested: is_horizontal_scroll_bar_show_requested show_tree_node_connectors -- Ensure connectors are displayed between nodes of tree structure in Current. require not_destroyed: not is_destroyed ensure tree_node_connectors_shown: are_tree_node_connectors_shown show_vertical_scroll_bar -- Ensure a vertical scroll bar is displayed in Current -- when required. Note that this does not force the vertical -- scroll bar to be visible, simply ensures that when `virtual_height` -- is greater than `viewable_height`, the scroll bar is displayed. require not_is_destroyed: not is_destroyed ensure is_vertical_scroll_bar_show_requested: is_vertical_scroll_bar_show_requested unlock_update -- Ensure `is_locked` is False, thereby ensuring graphical -- updates occur as normal. The complete client area -- is refreshed to synchronize the display with the contents. require not_is_destroyed: not is_destroyed ensure not_is_locked: not is_locked cell_unmerge_radio_button_groups (other: EV_CONTAINER) -- Remove other from radio button group of Current. -- If no radio button of other was checked before removal -- then first radio button contained will be checked. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed other_is_merged: attached cell_merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_groups.has (other) ensure -- from EV_CONTAINER other_not_merged: other.merged_radio_button_groups = Void not_contained_in_this_group: attached cell_merged_radio_button_groups as l_merged_r_b_groups implies not l_merged_r_b_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 (attached old cell_merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_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 -- Element change clear -- Remove all items from 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) -- Ensure that structure includes v. -- Do not move cursor. -- (from EV_CONTAINER) require -- from 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 -- from EV_CONTAINER has_v: cell_has (v) cell_fill (other: CONTAINER [EV_WIDGET]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from COLLECTION) require -- from COLLECTION other_not_void: other /= Void extendible: cell_extendible insert_new_column (a_index: INTEGER_32) -- Insert a new column immediately before column at index 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) -- Insert a new row immediately before row at index 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) -- Insert a new row immediately before row at index i and make that row a subnode of 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) -- Insert rows_to_insert rows immediately before row at index 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) -- Insert rows_to_insert new rows immediately before row at index i. -- Make these newly inserted rows subnodes of 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) -- Move column at index i and insert immediately before column at index j. -- To move column i to the last index in the grid, use 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) -- Move n columns starting at column i and insert immediately before column 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) -- Move row at index i immediately before row at index j. -- If j = row_count + 1 then row i is moved to the last index in the grid. -- Row i will be unparented if it has a 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) -- Move row at index i immediately before row at index j. -- Row i is re-parented as a subrow of a_parent_row. -- If j = row_count + 1 then row i is moved to the last index in the grid. 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) -- Move n rows starting at index i immediately before row at index j. -- If j = row_count + 1 the rows are moved to the very bottom of the grid. -- If `is_tree_enabled`, all rows moved that share the same tree structure depth -- as row i are unparented and set as root rows within the grid tree. -- All parent rows within the rows moved that have a tree structure depth -- greater than that of row i are left parented. 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) -- Move n rows starting at index i immediately before row at index j. -- All rows moved that share the same tree structure depth -- as row i are reparented as a subrow of a_parent_row. -- All parent rows within the rows moved that have a tree structure depth -- greater than that of row i are left parented. 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) -- Replace `item` with v. -- Was declared in {EV_CONTAINER} as synonym of replace. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: Writable v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: v /= Current v_not_parent_of_current: not cell_is_parent_recursive (v) v_containable: cell_may_contain (v) ensure -- from EV_CONTAINER has_v: cell_has (v) not_has_old_item: old Readable implies (attached old implementation.cell_item as l_item and then not cell_has (l_item)) remove_help_context -- Remove key press action associated with EV_APPLICATION.help_key. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed help_context_not_void: help_context /= Void ensure -- from EV_HELP_CONTEXTABLE no_help_context: help_context = Void remove_item (a_column, a_row: INTEGER_32) -- Remove grid item at position (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 -- Remove image displayed on Current. -- (from EV_PIXMAPABLE) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed ensure -- from EV_PIXMAPABLE pixmap_removed: cell_background_pixmap = Void remove_tooltip -- Make `tooltip` empty. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed ensure -- from EV_TOOLTIPABLE tooltip_removed: tooltip.is_empty cell_replace (v: like cell_item) -- Replace `item` with v. -- Was declared in {EV_CONTAINER} as synonym of put. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: Writable v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: v /= Current v_not_parent_of_current: not cell_is_parent_recursive (v) v_containable: cell_may_contain (v) ensure -- from EV_CONTAINER has_v: cell_has (v) not_has_old_item: old Readable implies (attached old implementation.cell_item as l_item and then not cell_has (l_item)) set_background_color (a_color: like background_color) -- Assign a_color to `background_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE background_color_assigned: background_color.is_equal (a_color) set_data (some_data: like data) -- Assign some_data to `data`. -- (from EV_ANY) require -- from EV_ANY not_destroyed: not is_destroyed ensure -- from EV_ANY data_assigned: data = some_data set_foreground_color (a_color: like foreground_color) -- Assign a_color to `foreground_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE foreground_color_assigned: foreground_color.is_equal (a_color) set_help_context (an_help_context: FUNCTION [EV_HELP_CONTEXT]) -- Assign an_help_context to `help_context`. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed an_help_context_not_void: an_help_context /= Void ensure -- from EV_HELP_CONTEXTABLE help_context_assigned: attached help_context as l_help_context and then l_help_context.is_equal (an_help_context) set_identifier_name (a_name: READABLE_STRING_GENERAL) -- Set `identifier_name` to a_name. -- (from EV_IDENTIFIABLE) require -- from EV_IDENTIFIABLE a_name_not_void: a_name /= Void a_name_not_empty: not a_name.is_empty no_period_in_name: not a_name.has ('.'.to_character_32) no_special_regexp_characters_in_name: ensure -- from EV_IDENTIFIABLE identifier_name_set: identifier_name.same_string_general (a_name) set_item (a_column, a_row: INTEGER_32; a_item: detachable EV_GRID_ITEM) -- Set grid item at position (a_column, a_row) to a_item. -- If a_item is Void, the current item (if any) is removed. 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) -- Set a_minimum_height in pixels to `minimum_height`. -- If `height` is less than a_minimum_height, resize. -- From now, `minimum_height` is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32) -- Assign a_minimum_height to `minimum_height` -- and a_minimum_width to `minimum_width` in pixels. -- If `width` or `height` is less than minimum size, resize. -- From now, minimum size is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user minimum_width_set_by_user_set: minimum_width_set_by_user set_minimum_width (a_minimum_width: INTEGER_32) -- Assign a_minimum_width in pixels to `minimum_width`. -- If `width` is less than a_minimum_width, resize. -- From now, `minimum_width` is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_width_set_by_user_set: minimum_width_set_by_user set_background_pixmap (a_pixmap: EV_PIXMAP) -- Display image of a_pixmap on Current. -- Image of pixmap will be a copy of a_pixmap. -- Image may be scaled in some descendents, i.e EV_TREE_ITEM -- See EV_TREE.set_pixmaps_size. -- (from EV_PIXMAPABLE) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed pixmap_not_void: a_pixmap /= Void set_pointer_style (a_cursor: EV_POINTER_STYLE) -- Assign a_cursor to `pointer_style`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_cursor_not_void: a_cursor /= Void ensure -- from EV_WIDGET pointer_style_assigned: attached pointer_style as l_pointer_style and then l_pointer_style.is_equal (a_cursor) set_tooltip (a_tooltip: READABLE_STRING_GENERAL) -- Assign a_tooltip to `tooltip`. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed tooltip: a_tooltip /= Void ensure -- from EV_TOOLTIPABLE tooltip_assigned: tooltip.same_string_general (a_tooltip) cloned: tooltip /= a_tooltip wipe_out -- Remove all columns and rows from Current. require not_destroyed: not is_destroyed ensure columns_removed: column_count = 0 rows_removed: row_count = 0 feature -- Removal dispose -- Free the entry associated with `object_id` if any -- (from IDENTIFIED) require -- from DISPOSABLE True ensure then -- from IDENTIFIED object_freed: id_freed frozen free_id -- Free the entry associated with `object_id` if any. -- (from IDENTIFIED) ensure -- from IDENTIFIED object_freed: id_freed cell_prune (v: EV_WIDGET) -- Remove v if contained. -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: Prunable v_not_void: v /= Void v_parent_void: v.parent = Current v_not_current: v /= Current ensure -- from EV_CONTAINER has_v: not cell_has (v) ensure then -- from EV_CELL not cell_has (v) cell_prune_all (v: EV_WIDGET) -- Remove all occurrences of v. -- (Reference or object equality, -- based on `object_comparison`.) -- (from COLLECTION) require -- from COLLECTION prunable: Prunable ensure -- from COLLECTION no_more_occurrences: not cell_has (v) remove_column (a_column: INTEGER_32) -- Remove column 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) -- Remove row a_row and all subrows recursively. -- If row (a_row).subrow_count_recursive is greater than 0 then -- all subrows of the row are also removed from 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) -- Remove all rows from lower_index to upper_index inclusive. 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 attached highest_parent_row_within_bounds (lower_index, upper_index) as l_row implies upper_index = l_row.index + l_row.subrow_count_recursive) or (is_tree_enabled and then highest_parent_row_within_bounds (lower_index, upper_index) = Void implies row (upper_index).subrow_count = 0) valid_final_row_in_tree_structure: (is_tree_enabled and then attached highest_parent_row_within_bounds (lower_index, upper_index) as l_row implies upper_index = l_row.index + l_row.subrow_count_recursive) or (is_tree_enabled and then highest_parent_row_within_bounds (lower_index, upper_index) = Void implies row (upper_index).subrow_count = 0) 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 -- Remove `item`. -- (from EV_CELL) require -- from COLLECTION prunable: Prunable ensure -- from COLLECTION wiped_out: cell_is_empty feature -- Conversion cell_linear_representation: LINEAR [like cell_item] -- Representation as a linear structure -- (from EV_CELL) feature -- Duplication frozen deep_copy (other: EV_GRID) -- Effect equivalent to that of: -- `copy` (other . `deep_twin`) -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY deep_equal: deep_equal (Current, other) frozen deep_twin: EV_GRID -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) frozen standard_copy (other: EV_GRID) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_standard_equal: standard_is_equal (other) frozen standard_twin: EV_GRID -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) frozen twin: EV_GRID -- New object equal to Current -- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations frozen default: detachable EV_GRID -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.`default` for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class cell_propagate_background_color -- Propagate `background_color` recursively, to all children. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER background_color_propagated: cell_background_color_propagated cell_propagate_foreground_color -- Propagate `foreground_color` recursively, to all children. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER foreground_color_propagated: cell_foreground_color_propagated refresh_now -- Force an immediate redraw of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed feature -- Implementation Changeable_comparison_criterion: BOOLEAN = False -- May `object_comparison` be changed? -- (Answer: no by default.) -- (from EV_CONTAINER) cl_extend (v: like cell_item) -- Ensure that structure includes v. -- (from EV_CONTAINER) require -- from COLLECTION extendible: cell_extendible ensure -- from COLLECTION item_inserted: cell_is_inserted (v) cl_prune (v: like cell_item) -- Remove one occurrence of v if any. -- (Reference or object equality, -- based on `object_comparison`.) -- (from EV_CONTAINER) require -- from COLLECTION prunable: Prunable cl_put (v: like cell_item) -- Replace `item` with v. -- (from EV_CONTAINER) require -- from COLLECTION extendible: cell_extendible ensure -- from COLLECTION item_inserted: cell_is_inserted (v) feature column_type: EV_GRID_COLUMN -- Type use for column objects. -- May be redefined by EV_GRID descendents. -- (from EV_GRID_TYPES) require -- from EV_GRID_TYPES callable: False row_type: EV_GRID_ROW -- Type used for row objects. -- May be redefined by EV_GRID descendents. -- (from EV_GRID_TYPES) require -- from EV_GRID_TYPES callable: False feature -- Activation Handling propagate_key_press (a_key: EV_KEY) -- Propagate key press for a_key to Current. -- Useful for handling custom navigation during item activation. require not_destroyed: not is_destroyed feature -- Command destroy -- Destroy underlying native toolkit object. -- Render Current unusable. -- (from EV_ANY) ensure -- from EV_ANY is_destroyed: is_destroyed feature -- Contract support are_columns_removable (a_index, n: INTEGER_32): BOOLEAN -- Are n columns starting at column index a_index removable from 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): detachable EV_GRID_ROW -- Return the highest level parent_row recursively of row upper_index -- that has an index greater or equal to 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 is_background_color_void: BOOLEAN -- If `background_color` void? -- (from EV_COLORIZABLE) is_bridge_ok (a_string: STRING_32): BOOLEAN -- If a_string equal implementation's `tooltip`? -- (from EV_TOOLTIPABLE) is_cloned (a_string: STRING_32): BOOLEAN -- If a_string same instance as implementation's `tooltip`? -- (from EV_TOOLTIPABLE) is_foreground_color_void: BOOLEAN -- If `foreground_color` void? -- (from EV_COLORIZABLE) is_in_default_state: BOOLEAN -- Is Current in its default state? require -- from EV_ANY True cell_is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN -- Is a_widget `parent`, or recursivly, `parent` of `parent`. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed cell_may_contain (v: EV_WIDGET): BOOLEAN -- May v be inserted in Current. -- Instances of EV_WINDOW may not be inserted -- in a container even though they are widgets. -- (from EV_CONTAINER) parent_of_source_allows_docking: BOOLEAN -- Does parent of source to be transported -- allow current to be dragged out? (See `real_source`) -- Not all Vision2 containers are currently supported by this -- mechanism, only descendents of EV_DOCKABLE_TARGET -- are supported. -- (from EV_DOCKABLE_SOURCE) rows_may_be_moved (a_first_row_index, a_row_count: INTEGER_32): BOOLEAN -- Do rows from a_first_row_index to a_first_row_index + a_row_count - 1 represent a complete tree structure? -- and if row (a_first_row_index) has a parent_row, are all rows to be moved nested within that parent -- within the tree structure? If Result is True, the rows may be moved without breaking an existing -- tree structure. 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 -- Does source recursively contain Current? -- As seen by parenting structure. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed source_not_void: source /= Void feature -- Event handling conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed after a dock completes from Current. -- Either to a dockable target or a dockable dialog. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a dockable source is dragged. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE -- Actions to be performed when a dockable source completes a transport -- Fired only if source has been moved, after parenting. -- (from EV_DOCKABLE_TARGET_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_TARGET_ACTION_SEQUENCES not_void: Result /= Void dpi_changed_actions: EV_DPI_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void file_drop_actions: EV_LITE_ACTION_SEQUENCE [LIST [STRING_32]] -- Actions to be performed when an OS file drop is performed on Current. -- (from EV_WIDGET_ACTION_SEQUENCES) focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is gained. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is lost. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE -- Actions to be performed when a keyboard press generates a displayable character. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_release_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE -- Actions to be performed when mouse wheel is rotated. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pick_actions: EV_PND_START_ACTION_SEQUENCE -- Actions to be performed when `pebble` is picked up. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE -- Actions to be performed when a transport from Current ends. -- If transport completed successfully, then event data -- is target. If cancelled, then event data is Void. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer is double clicked. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer enters widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer leaves widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE -- Actions to be performed when screen pointer moves. -- (from EV_WIDGET_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void resize_actions: EV_GEOMETRY_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void feature -- Iteration new_cursor: ITERATION_CURSOR [EV_WIDGET] -- Fresh cursor associated with current structure -- (from EV_CONTAINER) ensure -- from ITERABLE result_attached: Result /= Void feature -- Markers fixme (comment: READABLE_STRING_8) -- Mark code that has to be "fixed" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class to_implement (comment: READABLE_STRING_8) -- Mark code that has to be "implemented" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class to_implement_assertion (comment: READABLE_STRING_8): BOOLEAN -- Mark assertion that has to be "implemented" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class feature -- Measurements column_count: INTEGER_32 -- Number of columns in Current. require not_destroyed: not is_destroyed ensure result_not_negative: Result >= 0 displayed_column_count: INTEGER_32 -- Number of non-hidden columns displayed in Current. -- Equal to `column_count` if no columns have been -- hidden via `hide`. require not_destroyed: not is_destroyed ensure result_valid: Result >= 0 and Result <= column_count row_count: INTEGER_32 -- Number of rows in Current require not_destroyed: not is_destroyed ensure result_not_negative: Result >= 0 tree_node_spacing: INTEGER_32 -- Spacing value used around the expand/collapse node of a -- subrow. For example, to determine the height available for the node image -- within a subrow, subtract 2 * tree_node_spacing from the `row_height`. require not_destroyed: not is_destroyed ensure result_positive: Result >= 1 visible_row_count: INTEGER_32 -- Number of visible rows in Current. When `is_tree_enabled`, -- a number of rows may be within a collapsed parent row, so these -- are ignored. require not_destroyed: not is_destroyed ensure result_not_negative: Result >= 0 feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Status Report is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY) ensure -- from EV_ANY bridge_ok: Result = implementation.is_destroyed invariant -- from EV_CONTAINER client_width_non_negative: is_usable implies cell_client_width >= 0 client_width_within_limit: is_usable implies cell_client_width <= width client_height_non_negative: is_usable implies cell_client_height >= 0 client_height_within_limit: is_usable implies 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 -- from EV_WIDGET is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested parent_contains_current: is_usable and then attached parent as l_parent implies l_parent.has (Current) -- from EV_PICK_AND_DROPABLE user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1 -- from EV_ANY is_initialized: is_initialized default_create_called: default_create_called is_coupled: default_create_called implies (implementation.interface = Current or (attached {EV_ENVIRONMENT} Current and then attached implementation.interface)) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from EV_POSITIONED width_not_negative: is_usable implies width >= 0 height_not_negative: is_usable implies height >= 0 minimum_width_not_negative: is_usable implies minimum_width >= 0 minimum_height_not_negative: is_usable implies minimum_height >= 0 -- from EV_DOCKABLE_SOURCE parent_permits_docking: is_dockable implies parent_of_source_allows_docking -- from EV_COLORIZABLE background_color_not_void: is_usable implies not is_background_color_void foreground_color_not_void: is_usable implies not is_foreground_color_void note copyright: "Copyright (c) 1984-2014, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class EV_GRID -- Generated by Eiffel Studio --
For more details: eiffel.org