Automatic generation produced by ISE Eiffel
note description: "[ Widget which is a combination of an EV_TREE and an EV_MULTI_COLUMN_LIST. Implementation Interface. ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2021-11-18 05:22:34 -0900 (Thu, 18 Nov 2021) $" revision: "$Revision: 105966 $" deferred class interface EV_GRID_I feature -- Access accept_cursor: detachable EV_POINTER_STYLE -- Accept cursor set by user. -- To be displayed when the screen pointer is over a target that accepts -- `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE_I) actual_drop_target_agent: detachable FUNCTION [INTEGER_32, INTEGER_32, detachable EV_ABSTRACT_PICK_AND_DROPABLE] -- Overrides default drop target on a certain position. -- If Void, will use the default drop target. -- Always void if Current is not a widget. -- (from EV_WIDGET_I) are_tree_node_connectors_shown: BOOLEAN -- Are connectors between tree nodes shown in Current? frozen background_color: EV_COLOR -- Color displayed behind foreground features. -- (from EV_COLORIZABLE_I) client_height: INTEGER_32 -- Height of the client area of container. -- (from EV_CONTAINER_I) ensure -- from EV_CONTAINER_I positive: Result >= 0 client_width: INTEGER_32 -- Width of the client area of container. -- (from EV_CONTAINER_I) ensure -- from EV_CONTAINER_I positive: Result >= 0 column (a_column: INTEGER_32): EV_GRID_COLUMN -- Column at index a_column. require 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. configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY] -- (from EV_PICK_AND_DROPABLE_I) conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void count: INTEGER_32 -- Number of elements in Current. -- (from EV_CONTAINER_I) require -- from EV_CONTAINER_I not_destroyed: not is_destroyed default_key_processing_handler: detachable PREDICATE [EV_KEY] -- Agent used to determine whether the default key processing should occur for Current. -- If agent returns True then default key processing continues as normal, False prevents -- default key processing from occurring. -- (from EV_WIDGET_I) deny_cursor: detachable EV_POINTER_STYLE -- Deny cursor set by user. -- To be displayed when the screen pointer is not over a valid target. -- (from EV_PICK_AND_DROPABLE_I) 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 i_positive: i > 0 i_column_not_greater_than_displayed_column_count: i <= displayed_column_count ensure column_not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I 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` or `is_content_completely_dynamic. ev_application: EV_APPLICATION -- Current application if created yet. -- (from EV_SHARED_APPLICATION) require -- from EV_SHARED_APPLICATION application_exists: attached Shared_environment.application same_processor_as_application: Shared_environment.is_application_processor ev_separate_application: separate EV_APPLICATION -- Current application if created yet. -- (from EV_SHARED_APPLICATION) require -- from EV_SHARED_APPLICATION application_exists: attached Shared_environment.application frozen foreground_color: EV_COLOR -- Color of foreground features like text. -- (from EV_COLORIZABLE_I) generating_type: TYPE [detachable EV_GRID_I] -- 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 has (v: like cell_item): BOOLEAN -- Does structure include v? -- (from EV_CONTAINER_I) has_capture: BOOLEAN -- Does Current have capture? has_focus: BOOLEAN -- Does Current have focus? 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_I) ensure -- from EV_HELP_CONTEXTABLE_I current_if_exists: internal_help_context /= Void implies Result = internal_help_context interface_item: EV_WIDGET -- Current item but guaranteed attached for calling from interface only -- (from EV_CONTAINER_I) internal_pointer_style: EV_POINTER_STYLE -- Cursor displayed when screen pointer is over current widget, -- as seen from interface. -- (from EV_WIDGET_I) is_column_resize_immediate: BOOLEAN -- Is the user resizing of a reflected immediately in Current? -- If False, the column width is only updated upon completion of the resize. 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 content_requested_actions. The returned item is added -- to Current so the query only occurs once. is_dock_executing: BOOLEAN -- Is Current in the process of a dockable transport? -- (from EV_DOCKABLE_SOURCE_I) is_dockable: BOOLEAN -- Is Current dockable? -- (from EV_DOCKABLE_SOURCE_I) is_external_docking_enabled: BOOLEAN -- Is Current able to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of the transport? -- (from EV_DOCKABLE_SOURCE_I) is_external_docking_relative: BOOLEAN -- Will dockable dialog displayed when Current is docked externally -- be displayed relative to parent window of Current? -- Otherwise displayed as a standard window. -- (from EV_DOCKABLE_SOURCE_I) is_header_displayed: BOOLEAN -- Is the header displayed in Current. 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. 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. is_resizing_divider_enabled: BOOLEAN -- Is a vertical divider displayed during column resizing? 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. is_row_height_fixed: BOOLEAN -- Must all rows in Current have the same height? 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. 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. cell_item: detachable EV_WIDGET -- Current item. -- (from EV_CONTAINER_I) item (a_column: INTEGER_32; a_row: INTEGER_32): detachable EV_GRID_ITEM -- Cell at a_column and a_row position, Void if none. require a_column_positive: a_column > 0 a_column_not_greater_than_column_count: a_column <= column_count a_row_positive: a_row > 0 a_row_not_greater_than_row_count: a_row <= row_count 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. locked_indexes: ARRAYED_LIST [EV_GRID_LOCKED_I] -- Sorted array of all columns and rows currently locked. 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`. ensure result_non_negative: Result >= 0 maximum_virtual_y_position: INTEGER_32 -- Maximum permitted virtual y position based on current properties. -- Properties that affect this value are `is_horizontal_scrolling_per_item` and -- `is_horizontal_overscroll_enabled`. ensure result_non_negative: Result >= 0 merged_radio_button_groups: detachable ARRAYED_LIST [EV_CONTAINER] -- Result is all other radio button groups -- merged with Current. -- (from EV_CONTAINER_I) ensure -- from EV_CONTAINER_I current_not_included: Result /= Void implies not Result.has (attached_interface) not_external_docking_enabled: BOOLEAN -- Attribute used for is_externally_dockable. We must implement -- is_externally_dockable this way as we have no easy solution to -- assign True to is_externally_dockable. -- (from EV_DOCKABLE_SOURCE_I) not_is_external_docking_relative: BOOLEAN -- Will dockable dialog displayed when Current is docked externally -- be displayed relative to parent window of Current? -- Otherwise displayed as a standard window. -- Internal reversed value of `is_external_docking_relative` as we cannot -- easily initialize a BOOLE to True in this case. -- (from EV_DOCKABLE_SOURCE_I) original_parent_position: INTEGER_32 -- Original position in parent. Required -- to restore widget later. -- (from EV_DOCKABLE_SOURCE_I) parent: detachable EV_CONTAINER -- Container widget that contains Current. -- (Void if Current is not in a container) -- (from EV_WIDGET_I) pebble: detachable ANY -- Data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) pebble_function: detachable FUNCTION [detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) pebble_positioning_enabled: BOOLEAN -- If True then pick and drop start coordinates are -- `pebble_x_position`, `pebble_y_position`. -- If False then pick and drop start coordinates are -- the pointer coordinates. -- (from EV_PICK_AND_DROPABLE_I) pebble_x_position: INTEGER_32 -- Initial x position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) pebble_y_position: INTEGER_32 -- Initial y position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) pick_actions: EV_PND_START_ACTION_SEQUENCE -- Actions to be performed when `pebble` is picked up. ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I 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. ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void pixels_displayed_after_final_column: INTEGER_32 -- Width in pixels displayed after the final column of Current. -- If is_horizontal_overdraw_enabled this is `viewable_width` less the final column width. -- If not is_horizontal_overdraw_enabled and `is_horizontal_scrolling_per_item` this is -- the number of pixels required to ensure the first visible column is flush to the left of the -- viewable area of Current. pixels_displayed_after_final_row: INTEGER_32 -- Height in pixels displayed after the final row of Current. -- If is_vertical_overdraw_enabled this is `viewable_height` less the final row height. -- If not is_vertical_overdraw_enabled and `is_vertical_scrolling_per_item` this is -- the number of pixels required to ensure the first visible row is flush to the top of the -- viewable area of Current. ensure result_non_negative: Result >= 0 result_no_more_than_viewable_height: Result <= viewable_height no_rows_contained_implies_result_is_viewable_height: row_count = 0 implies Result = viewable_height valid_result_with_rows_with_overdraw_with_fixed_row_height: row_count > 0 and is_row_height_fixed and is_vertical_overscroll_enabled implies Result = viewable_height - row_height valid_result_with_rows_when_per_pixel_scrolling_with_no_overdraw: row_count > 0 and not is_vertical_scrolling_per_item and not is_vertical_overscroll_enabled implies Result = 0 valid_result_with_fixed_height_rows_when_per_item_scrolling_and_no_overdraw: row_count > 0 and is_row_height_fixed and is_vertical_scrolling_per_item and is_vertical_scrolling_per_item and row (row_count).virtual_y_position + row_height > viewable_height and not is_vertical_overscroll_enabled implies Result <= row_height background_pixmap: detachable EV_PIXMAP -- Image displayed on Current. -- (from EV_PIXMAPABLE_I) pointer_position: EV_COORDINATE -- Position of the screen pointer relative to Current. -- (from EV_WIDGET_I) ensure -- from EV_WIDGET_I result_not_void: Result /= Void pointer_style: detachable EV_POINTER_STYLE -- Cursor displayed when screen pointer is over current widget. -- Void if none has been set using set_pointer_position. -- (from EV_WIDGET_I) real_source: detachable EV_DOCKABLE_SOURCE -- Result is EV_DOCKABLE_SOURCE which should be -- dragged when docking begins on Current. -- (from EV_DOCKABLE_SOURCE_I) real_target: detachable EV_DOCKABLE_TARGET -- Result is target used during a dockable transport if -- mouse pointer is above Current. -- (from EV_WIDGET_I) remove_selection -- Ensure that `selected_rows` and `selected_items` are empty. 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 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. 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. selected_columns: ARRAYED_LIST [EV_GRID_COLUMN] -- All columns selected in Current. ensure result_not_void: Result /= Void selected_items: ARRAYED_LIST [EV_GRID_ITEM] -- All items selected in Current. ensure result_not_void: Result /= Void selected_rows: ARRAYED_LIST [EV_GRID_ROW] -- All rows selected in Current. ensure result_not_void: Result /= Void set_default_key_processing_handler (a_handler: like default_key_processing_handler) -- Assign `default_key_processing_handler` to a_handler. Shared_environment: EV_ENVIRONMENT -- Shared EV_ENVIRONMENT object. -- (from EV_SHARED_APPLICATION) subrow_indent: INTEGER_32 -- Number of pixels horizontally by which each subrow is indented -- from its parent_row. tooltip: STRING_32 -- Tooltip displayed on Current. unlock_column (a_column: EV_GRID_COLUMN_I) -- Ensure column a_column is unlocked. ensure column_not_locked: not a_column.is_locked unlock_row (a_row: EV_GRID_ROW_I) -- Ensure row a_row is unlocked. ensure a_row_not_locked: not a_row.is_locked 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. -- Is equivalent to viewport.height and by storing this, multiple queries are far quicker -- as the grid is only resized periodically and we no longer have to call EiffelVision for the value. viewable_width: INTEGER_32 -- Width of Current available to view displayed items. Does -- not include width of any displayed scroll bars. Is equivalent to viewport.width and -- by storing this, multiple queries are far quicker as the grid is only resized periodically -- and we no longer have to call EiffelVision for the value. 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. 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. ensure viewable_y_offset_valid: Result >= 0 and Result <= height virtual_height: INTEGER_32 -- Height of virtual area in pixels. ensure result_non_negative: Result >= 0 virtual_width: INTEGER_32 -- Width of virtual area in pixels. 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. 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. ensure valid_result: Result >= 0 and Result <= maximum_virtual_y_position feature -- Measurement dpi: NATURAL_32 -- Window dpi. -- (from EV_POSITIONED_I) height: INTEGER_32 -- Vertical size in pixels. -- (from EV_POSITIONED_I) minimum_height: INTEGER_32 -- Minimum vertical size in pixels. -- (from EV_POSITIONED_I) minimum_width: INTEGER_32 -- Minimum horizontal size in pixels. -- (from EV_POSITIONED_I) screen_x: INTEGER_32 -- Horizontal offset relative to screen. -- (from EV_WIDGET_I) screen_y: INTEGER_32 -- Vertical offset relative to screen. -- (from EV_WIDGET_I) width: INTEGER_32 -- Horizontal size in pixels. -- (from EV_POSITIONED_I) x_position: INTEGER_32 -- Horizontal offset relative to parent `x_position` in pixels. -- (from EV_POSITIONED_I) y_position: INTEGER_32 -- Vertical offset relative to parent `y_position` in pixels. -- (from EV_POSITIONED_I) feature -- Comparison frozen deep_equal (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_I): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) is_equal (other: EV_GRID_I): BOOLEAN -- Is other attached to an object considered -- equal to current object? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ 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_I): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report 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. closest_dockable_target: detachable EV_DOCKABLE_TARGET -- Result is first dockable target that `is_dockable` found by recursively -- searching up through the parenting structure from the widget -- currently underneath the pointer position. -- Result will be Void if a dockable target is not found. -- (from EV_DOCKABLE_SOURCE_I) ensure -- from EV_DOCKABLE_SOURCE_I result_is_dockable: Result /= Void implies Result.is_docking_enabled 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 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 depth_in_tree (a_row_index: INTEGER_32): INTEGER_32 -- Depth in tree for a_row_index require valid_index: 0 < a_row_index and a_row_index <= row_count disable_capture -- Release the user input. displayed_background_color (a_column, a_row: INTEGER_32): EV_COLOR -- Result is background color to be displayed for item at position a_column, a_row -- on parts of the cell space in which the item is not displayed. i.e. for the background -- area of a tree structure. require valid_column: a_column >= 1 and a_column <= column_count valid_row: a_row >= 1 and a_row <= row_count ensure result_not_void: Result /= Void drawables_have_focus: BOOLEAN -- Does `drawable` or any of the drawables representing locked rows currently -- have the focus? If False then selection should be grayed. enable_capture -- Grab the user input. 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 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 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 focused_selection_color: EV_COLOR -- Color used to show selection within items while focused. focused_selection_text_color: EV_COLOR -- Color used to show selection within items while focused. get_next_target (a_widget: EV_WIDGET): detachable EV_DOCKABLE_TARGET -- Result is next dockable target that is `is_dockable` found by -- recursively seraching up the parenting structure from current_target. -- Result will be Void if none. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I a_widget_not_void: a_widget /= Void ensure -- from EV_DOCKABLE_SOURCE_I result_is_dockable: Result /= Void implies Result.is_docking_enabled has_selected_column: BOOLEAN -- Has selected column? has_selected_item: BOOLEAN -- Has selected items? has_selected_row: BOOLEAN -- Has selected row? internal_non_sensitive: BOOLEAN -- Is Current not sensitive to input as seen -- from `interface`? -- (from EV_SENSITIVE_I) is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY_I) is_docking_enabled: BOOLEAN -- May Current be docked to? -- (from EV_DOCKABLE_TARGET_I) is_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? is_multiple_row_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select a row, with multiple -- row selection permitted via the use of Ctrl and Shift keys? is_multiple_selection_enabled: BOOLEAN -- Is Current in either multiple item or row selection mode? is_row_selection_enabled: BOOLEAN -- Is Current in either single or multiple row selection mode? is_selection_keyboard_handling_enabled: BOOLEAN -- May an item be selected via the keyboard? is_selection_on_click_enabled: BOOLEAN -- Will an item be selected if clicked upon by the user? is_selection_on_single_button_click_enabled: BOOLEAN -- Will an item be selected if clicked upon via mouse button 1 only. -- Mouse buttons 1 and 2 will leave selection unchanged. is_single_item_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select an item, unselecting -- any previously selected items? is_single_row_selection_enabled: BOOLEAN -- Does clicking or keyboard navigating via arrow keys select a row, unselecting -- any previously selected row? is_transport_enabled: BOOLEAN -- Is the transport mechanism enabled? -- (from EV_PICK_AND_DROPABLE_I) is_tree_enabled: BOOLEAN -- Is tree functionality enabled? last_visible_column: detachable EV_GRID_COLUMN -- Last column visible in Current or Void if `column_count` = 0 -- The last visible column may be only partially visible. require 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 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 mode_is_configurable_target_menu: BOOLEAN -- Is the transport mechanism a configurable target menu? -- (from EV_PICK_AND_DROPABLE_I) mode_is_drag_and_drop: BOOLEAN -- Is the transport mechanism drag and drop? -- (from EV_PICK_AND_DROPABLE_I) mode_is_pick_and_drop: BOOLEAN -- Is the transport mechanism pick and drop? -- (from EV_PICK_AND_DROPABLE_I) mode_is_target_menu: BOOLEAN -- Is the transport mechanism a target menu? -- (from EV_PICK_AND_DROPABLE_I) non_focused_selection_color: EV_COLOR -- Color used to show selection within items while not focused. non_focused_selection_text_color: EV_COLOR -- Color used for text of selected items while not focused. 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. user_is_sensitive: BOOLEAN -- Is the object sensitive to user input. -- (from EV_SENSITIVE_I) veto_dock_function: detachable FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN] -- Function used to veto transport. -- (from EV_DOCKABLE_TARGET_I) viewable_row_indexes: ARRAYED_LIST [INTEGER_32] -- Row indexes 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. ensure result_not_void: Result /= Void visible_column_indexes: ARRAYED_LIST [INTEGER_32] -- All columns that are currently visible in Current. require is_displayed: is_displayed ensure result_not_void: Result /= Void visible_row_indexes: ARRAYED_LIST [INTEGER_32] -- All rows that are currently visible in Current. require is_displayed: is_displayed ensure result_not_void: Result /= Void feature -- Status setting activate_item (a_item: EV_GRID_ITEM) -- Setup a_item for user interactive editing. require a_item_not_void: a_item /= Void activate_window: detachable EV_POPUP_WINDOW -- Window used to edit grid item contents on activate. currently_active_item: detachable EV_GRID_ITEM -- Item that is currently active. deactivate_item (a_item: EV_GRID_ITEM) -- Cleanup from previous call to activate. require a_item_not_void: a_item /= Void disable_always_selected -- Allow the user to completely remove the selection from the grid by clicking on an item, -- clicking on a Void area or by Ctrl clicking the selected item itself. disable_column_resize_immediate -- Ensure `is_column_resize_immediate` is False. ensure not_is_column_resize_immediate: not is_column_resize_immediate disable_column_separators -- Ensure `are_column_separators_enabled` is False. ensure column_separators_disabled: not are_column_separators_enabled disable_columns_drawn_above_rows -- Ensure `are_columns_drawn_above_rows` is False. ensure columns_drawn_below_rows: not are_columns_drawn_above_rows disable_dockable -- Ensure Current is not dockable -- (from EV_DOCKABLE_SOURCE_I) ensure -- from EV_DOCKABLE_SOURCE_I not_is_dockable: not is_dockable disable_docking -- Ensure `is_docking_enabled` is False. -- Current will not accept docking. -- (from EV_DOCKABLE_TARGET_I) require -- from EV_DOCKABLE_TARGET_I application_exists: attached (create {EV_ENVIRONMENT} end).application ensure -- from EV_DOCKABLE_TARGET_I not_dockable: not is_docking_enabled id_not_stored_in_application: attached (create {EV_ENVIRONMENT} end).application as l_application and then not l_application.implementation.dockable_targets.has (attached_interface.object_id) disable_dynamic_content -- Ensure contents of Current are not dynamic and are no longer retrieved as such. ensure content_not_dynamic: not is_content_partially_dynamic disable_external_docking -- Forbid Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of the transport? -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE_I not_externally_dockable: not is_external_docking_enabled disable_external_docking_relative -- Assign False to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed as a standard window. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE_I external_docking_not_relative: not is_external_docking_relative disable_full_redraw_on_virtual_position_change -- Ensure `is_full_redraw_on_virtual_position_change_enabled` is False. 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. 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. 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. disable_pebble_positioning -- Assign False to `pebble_positioning_enabled`. -- (from EV_PICK_AND_DROPABLE_I) disable_resizing_divider -- Ensure no vertical divider is displayed during column resizing. ensure resizing_divider_disabled: not is_resizing_divider_enabled disable_row_height_fixed -- Permit rows to have varying heights. require not_dynamic_content_enabled_with_height_not_bounded: not (is_content_partially_dynamic and not is_vertical_overscroll_enabled) disable_row_separators -- Ensure `are_row_separators_enabled` is False. ensure row_separators_disabled: not are_row_separators_enabled disable_selection_keyboard_handling -- Disable selection handling of items via the keyboard. ensure selection_keyboard_handling_disabled: not is_selection_keyboard_handling_enabled disable_selection_on_click -- Disable selection handling when items are clicked upon. ensure selection_on_click_disabled: not is_selection_on_click_enabled disable_solid_resizing_divider -- Ensure resizing divider displayed during column resizing -- is displayed as a dashed line. ensure dashed_resizing_divider: not is_resizing_divider_solid disable_transport -- Deactivate pick/drag and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I is_transport_disabled: not is_transport_enabled disable_tree -- Disable tree functionality for Current. -- All subrows of rows contained are unparented, -- which flattens the tree structure. ensure tree_disabled: not is_tree_enabled disable_vertical_overscroll -- Ensure `is_vertical_overscroll_enabled` is False. require 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. 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. enable_column_resize_immediate -- Ensure `is_column_resize_immediate` is True. ensure is_column_resize_immediate: is_column_resize_immediate enable_column_separators -- Ensure `are_column_separators_enabled` is True. ensure column_separators_enabled: are_column_separators_enabled enable_columns_drawn_above_rows -- Ensure `are_columns_drawn_above_rows` is True. ensure columns_drawn_above_rows: are_columns_drawn_above_rows enable_dockable -- Allow Current to be dockable -- (from EV_DOCKABLE_SOURCE_I) ensure -- from EV_DOCKABLE_SOURCE_I is_dockable: is_dockable enable_docking -- Ensure `is_docking_enabled` is True. -- Current will accept docking from a -- compatible EV_DOCKABLE_SOURCE. -- (from EV_DOCKABLE_TARGET_I) require -- from EV_DOCKABLE_TARGET_I application_exists: attached (create {EV_ENVIRONMENT} end).application ensure -- from EV_DOCKABLE_TARGET_I is_dockable: is_docking_enabled id_stored_in_application: attached (create {EV_ENVIRONMENT} end).application as l_application and then l_application.implementation.dockable_targets.has (attached_interface.object_id) enable_external_docking -- Allow Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of the transport? -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE_I is_externally_dockable: is_external_docking_enabled enable_external_docking_relative -- Assign True to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed relative to the top level window. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE_I external_docking_not_relative: is_external_docking_relative enable_full_redraw_on_virtual_position_change -- Ensure `is_full_redraw_on_virtual_position_change_enabled` is True. 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. ensure is_horizontal_overscroll_enabled: is_horizontal_overscroll_enabled enable_horizontal_scrolling_per_item -- Ensure horizontal scrolling is performed on a per-item basis. ensure horizontal_scrolling_performed_per_item: is_horizontal_scrolling_per_item enable_item_tab_navigation -- Ensure that tab navigation occurs for each navigatable item. 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. 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. ensure multiple_row_selection_enabled: is_multiple_row_selection_enabled enable_partial_dynamic_content -- Ensure contents of Current must be retrieved when required via -- content_requested_actions only if the item is not already set -- in Current. require 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`. -- (from EV_PICK_AND_DROPABLE_I) enable_resizing_divider -- Ensure a vertical divider is displayed during column resizing. ensure resizing_divider_enabled: is_resizing_divider_enabled enable_row_height_fixed -- Ensure all rows have the same height. enable_row_separators -- Ensure `are_row_separators_enabled` is True. ensure row_separators_enabled: are_row_separators_enabled enable_selection_keyboard_handling -- Enable selection handling of items via the keyboard. ensure selection_keyboard_handling_enabled: is_selection_keyboard_handling_enabled enable_selection_on_click -- Enable selection handling of items when clicked upon. ensure selection_on_click_enabled: is_selection_on_click_enabled enable_selection_on_single_button_click -- Enable selection handling of items when clicked upon via mouse button 1. -- This is useful for implementing Contextual Menus where the selection may need -- to remain unchanged when using mouse button 3 for instance. ensure selection_on_single_click_enabled: is_selection_on_single_button_click_enabled and then is_selection_on_click_enabled enable_single_item_selection -- Allow the user to select a single item via clicking or navigating using the keyboard arrow keys. 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. 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. ensure solid_resizing_divider: is_resizing_divider_solid enable_transport -- Activate pick/drag and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) require -- from EV_PICK_AND_DROPABLE_I pebble_not_void: pebble /= Void or pebble_function /= Void ensure -- from EV_PICK_AND_DROPABLE_I is_transport_enabled: is_transport_enabled enable_tree -- Enable tree functionality for Current. -- Must be True to perform any tree structure functions on Current. -- Use `enable_tree` and `disable_tree` to set this state. ensure tree_enabled: is_tree_enabled enable_vertical_overscroll -- Ensure `is_vertical_overscroll_enabled` is True. ensure is_vertical_overscroll_enabled: is_vertical_overscroll_enabled enable_vertical_scrolling_per_item -- Ensure vertical scrolling is performed on a per-item basis. ensure vertical_scrolling_performed_per_item: is_vertical_scrolling_per_item has_horizontal_scrolling_per_item_just_changed: BOOLEAN -- Has the horizontal scrolling method just been changed between -- per item and per pixel? This is used to adjust the scroll bar's position -- to approximate it's original position during the recomputation of it's -- settings in `recompute_horizontal_scroll_bar`. has_vertical_scrolling_per_item_just_changed: BOOLEAN -- Has the vertical scrolling method just been changed between -- per item and per pixel? This is used to adjust the scroll bar's position -- to approximate it's original position during the recomputation of it's -- settings in `recompute_vertical_scroll_bar`. hide -- Request that Current not be displayed when its parent is. -- (from EV_WIDGET_I) hide_column (a_column: INTEGER_32) -- Ensure column a_column is not visible in Current. require 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. ensure header_not_displayed: not is_header_displayed hide_horizontal_scroll_bar -- Ensure no horizontal scroll bar is displayed in Current -- at any time. 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. 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. ensure not_is_vertical_scroll_bar_show_requested: not is_vertical_scroll_bar_show_requested internal_disable_dockable -- Platform specific implementation of `disable_dockable`. -- (from EV_DOCKABLE_SOURCE_I) internal_enable_dockable -- Platform specific implementation of `enable_dockable`. -- (from EV_DOCKABLE_SOURCE_I) is_always_selected: BOOLEAN -- Ensure that the user may not completely remove the selection from Current. is_horizontal_scroll_bar_show_requested: BOOLEAN -- Will a horizontal scroll bar be displayed in Current when -- `virtual_width` exceeds `viewable_width`? is_item_height_changing: BOOLEAN -- Is height of items in Current changing? is_item_tab_navigation_enabled: BOOLEAN -- Is item navigation enabled for tabbing between items? is_vertical_scroll_bar_show_requested: BOOLEAN -- Will a vertical scroll bar be displayed in Current when -- `virtual_height` exceeds `viewable_height`? item_pebble_function: detachable FUNCTION [detachable EV_GRID_ITEM, detachable ANY] -- User pebble function lock_update -- Ensure `is_locked` is True, thereby preventing graphical -- updates until `unlock_update` is called. ensure is_locked: is_locked merge_radio_button_groups (other: EV_CONTAINER) -- Merge Current radio button group with that of other. -- (from EV_CONTAINER_I) redraw -- Force Current to be re-drawn when next idle. remove_default_key_processing_handler -- Ensure `default_key_processing_handler` is Void. -- (from EV_WIDGET_I) ensure -- from EV_WIDGET_I default_key_processing_handler_removed: default_key_processing_handler = Void remove_pebble -- Remove `pebble`. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pebble_removed: pebble = Void and pebble_function = Void is_transport_disabled: not is_transport_enabled remove_real_source -- Ensure `real_source` is Void. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE_I real_source_void: real_source = Void remove_real_target -- Ensure `real_target` is Void. -- (from EV_WIDGET_I) ensure -- from EV_WIDGET_I real_target_void: real_target = Void reset_pebble_function -- Reset any values created by calling `pebble_function`. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pebble_function_preserved: pebble_function = old pebble_function pebble_without_function: pebble_function = Void implies (pebble = old pebble) pebble_with_function: pebble_function /= Void implies pebble = Void select_column (a_column: INTEGER_32) -- Ensure all items in a_column are selected. require 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 a_row_within_bounds: a_row > 0 and a_row <= row_count ensure row_selected: row (a_row).is_selected set_actual_drop_target_agent (an_agent: like actual_drop_target_agent) -- Assign an_agent to `actual_drop_target_agent`. -- (from EV_WIDGET_I) require -- from EV_WIDGET_I an_agent_not_void: an_agent /= Void ensure -- from EV_WIDGET_I assigned: actual_drop_target_agent = an_agent set_column_count_to (a_column_count: INTEGER_32) -- Resize Current to have a_column_count columns. require a_column_count_not_negative: a_column_count >= 0 ensure column_count_set: column_count = a_column_count set_configurable_target_menu_handler (a_handler: like configurable_target_menu_handler) -- Set Configurable Target Menu Handler to a_handler. set_configurable_target_menu_mode -- Set transport mechanism to a configurable target_menu. ensure -- from EV_PICK_AND_DROPABLE_I mode_is_target_menu: mode_is_configurable_target_menu set_default_colors -- Set foreground and background color to their default values. set_drag_and_drop_mode -- Set transport mechanism to drag and drop, ensure -- from EV_PICK_AND_DROPABLE_I mode_is_drag_and_drop: 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` or `is_content_completely_dynamic. require 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 valid_row_index: a_row >= 1 and a_row <= row_count set_focus -- Grab keyboard focus. set_focused_selection_color (a_color: EV_COLOR) -- Assign a_color to `focused_selection_color`. require 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 a_color_not_void: a_color /= Void ensure focused_selection_text_color_set: focused_selection_text_color = a_color 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 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 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 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`. require -- from EV_PICK_AND_DROPABLE_I a_pebble_not_void: a_pebble /= Void ensure -- from EV_PICK_AND_DROPABLE_I pebble_assigned: pebble = a_pebble is_transport_enabled: is_transport_enabled set_pebble_function (a_function: FUNCTION [detachable ANY]) -- Assign a_function to `pebble_function`. require -- from EV_PICK_AND_DROPABLE_I a_function_not_void: a_function /= Void ensure -- from EV_PICK_AND_DROPABLE_I pebble_function_assigned: pebble_function = a_function is_transport_enabled: is_transport_enabled set_pebble_position (a_x, a_y: INTEGER_32) -- Set the initial position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pick_x_assigned: pick_x.to_integer_32 = a_x pick_y_assigned: pick_y.to_integer_32 = a_y set_pick_and_drop_mode -- Set transport mechanism to pick and drop, ensure -- from EV_PICK_AND_DROPABLE_I mode_is_pick_and_drop: mode_is_pick_and_drop set_real_source (dockable_source: EV_DOCKABLE_SOURCE) -- Set dockable_source to be the widget moved when a -- drag begins on Current. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I is_dockable: is_dockable dockable_source_not_void: dockable_source /= Void ensure -- from EV_DOCKABLE_SOURCE_I real_source_assigned: real_source = dockable_source set_real_target (a_target: EV_DOCKABLE_TARGET) -- Assign a_target to `real_target`. -- (from EV_WIDGET_I) require -- from EV_WIDGET_I target_not_void: a_target /= Void ensure -- from EV_WIDGET_I assigned: real_target = a_target set_row_count_to (a_row_count: INTEGER_32) -- Resize Current to have a_row_count columns. require 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 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 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 a_subrow_indent_non_negtive: a_subrow_indent >= 0 ensure subrow_indent_set: subrow_indent = a_subrow_indent set_target_menu_mode -- Set transport mechanism to a target_menu. ensure -- from EV_PICK_AND_DROPABLE_I mode_is_target_menu: mode_is_target_menu set_tree_node_connector_color (a_color: EV_COLOR) -- Set a_color as `tree_node_connector_color`. require 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: detachable FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN]) -- Assign a_function to `veto_dock_function`. -- (from EV_DOCKABLE_TARGET_I) require -- from EV_DOCKABLE_TARGET_I a_function_not_void: a_function /= Void ensure -- from EV_DOCKABLE_TARGET_I veto_function_set: veto_dock_function = a_function set_virtual_position (virtual_x, virtual_y: INTEGER_32) -- Move Current to virtual position virtual_x, virtual_y. require 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. -- (from EV_WIDGET_I) show_column (a_column: INTEGER_32) -- Ensure column a_column is visible in Current. require 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_I) show_header -- Ensure header displayed. 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. 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. 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. 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. ensure not_is_locked: not is_locked unmerge_radio_button_groups (other: EV_CONTAINER) -- Remove other from radio button group of Current. -- (from EV_CONTAINER_I) user_disable_sensitive -- Make object desensitive to user input. -- (from EV_SENSITIVE_I) ensure -- from EV_SENSITIVE_I is_desensitive: not user_is_sensitive user_enable_sensitive -- Make object sensitive to user input. -- (from EV_SENSITIVE_I) ensure -- from EV_SENSITIVE_I is_sensitive_if_parent_sensitive: (has_parent and then parent_is_sensitive) implies attached_interface.implementation.is_sensitive is_sensitive_if_orphaned: not has_parent implies attached_interface.implementation.is_sensitive feature -- Element change disable_drawables_have_focus -- Ensure `drawables_have_focus` is set to False. ensure drawables_have_focus: not drawables_have_focus enable_drawables_have_focus -- Ensure `drawables_have_focus` is set to True. ensure drawables_have_focus: drawables_have_focus extend (an_item: like cell_item) -- Ensure that structure includes an_item. -- (from EV_CELL_I) require -- from EV_CONTAINER_I v_not_void: an_item /= Void insert_new_column (a_index: INTEGER_32) -- Insert a new column at index a_index. require a_index_within_range: a_index > 0 and a_index <= column_count + 1 ensure column_count_set: column_count = old column_count + 1 insert_new_rows (rows_to_insert, i: INTEGER_32) -- Insert rows_to_insert rows at index i. require 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 at index i and make those rows subnodes of a_parent_row. require i_positive: i > 0 tree_enabled: is_tree_enabled rows_to_insert_positive: row_count >= 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_columns (i, j, n: INTEGER_32) -- Move n columns at index i to index j. require 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) 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_rows_to_parent (i, j, n: INTEGER_32; a_parent_row: detachable EV_GRID_ROW) -- All purpose row moving routine. -- 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 reparented as a subrow of a_parent_row. -- If a_parent_row is Void then they are set as root nodes of 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 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) not_breaking_existing_subrow_structure: j = row_count + 1 or else (a_parent_row = Void and j <= row_count and i + n <= row_count and ((j = i or j = i + 1) implies row (i + n).parent_row = Void)) or else ((a_parent_row = Void and j <= row_count) implies row (j).parent_row = Void) j_valid_for_move_to_a_parent_row: a_parent_row /= Void implies ((j = i + n and then (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: (a_parent_row /= Void and then 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 pixmap_equal_to (a_pixmap: EV_PIXMAP): BOOLEAN -- Is a_pixmap equal to pixmap? -- (from EV_PIXMAPABLE_I) remove_help_context -- Remove key press action associated with EV_APPLICATION.help_key. -- (from EV_HELP_CONTEXTABLE_I) require -- from EV_HELP_CONTEXTABLE_I help_context_not_void: help_context /= Void ensure -- from EV_HELP_CONTEXTABLE_I no_help_context: internal_help_context = Void remove_background_pixmap -- Make pixmap Void. -- (from EV_PIXMAPABLE_I) ensure -- from EV_PIXMAPABLE_I pixmap_removed: background_pixmap = Void replace (v: detachable like cell_item) -- Replace `item` with v. -- (from EV_CONTAINER_I) reset_minimum_height -- Reset the minimum height. -- (from EV_WIDGET_I) reset_minimum_size -- Reset the minimum size (width and height). -- (from EV_WIDGET_I) reset_minimum_width -- Reset the minimum width. -- (from EV_WIDGET_I) set_background_color (a_color: like background_color) -- Assign a_color to `foreground_color`. -- (from EV_COLORIZABLE_I) require -- from EV_COLORIZABLE_I a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE_I background_color_assigned: is_initialized implies background_color.is_equal (a_color) set_foreground_color (a_color: like foreground_color) -- Assign a_color to `foreground_color`. -- (from EV_COLORIZABLE_I) require -- from EV_COLORIZABLE_I a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE_I foreground_color_assigned: is_initialized implies foreground_color.is_equal (a_color) set_help_context (an_help_context: like help_context) -- Assign a_help_context to `help_context`. -- Assign an_help_context to `help_context`. -- (from EV_HELP_CONTEXTABLE_I) require -- from EV_HELP_CONTEXTABLE_I an_help_context_not_void: an_help_context /= Void ensure -- from EV_HELP_CONTEXTABLE_I help_context_assigned: attached help_context as l_help_context and then l_help_context ~ an_help_context 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 a_column_positive: a_column > 0 a_row_positive: a_row > 0 a_item_not_parented: a_item /= Void implies a_item.parent = Void valid_tree_structure_on_item_insertion: a_item /= Void and is_tree_enabled and then a_row <= row_count and then attached row (a_row).parent_row as l_parent_row implies a_column >= l_parent_row.index_of_first_item 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 the minimum vertical size to a_minimum_height in pixels. -- (from EV_WIDGET_I) require -- from EV_WIDGET_I a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET_I minimum_height_assigned: is_usable implies ((a_minimum_height > 0 implies attached_interface.minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (attached_interface.minimum_height <= 1))) set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32) -- Set the minimum horizontal size to a_minimum_width in pixels. -- Set the minimum vertical size to a_minimum_height in pixels. -- (from EV_WIDGET_I) require -- from EV_WIDGET_I a_minimum_width_positive: a_minimum_width >= 0 a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET_I minimum_width_assigned: is_usable implies ((a_minimum_width > 0 implies attached_interface.minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (attached_interface.minimum_width <= 1))) minimum_height_assigned: is_usable implies ((a_minimum_height > 0 implies attached_interface.minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (attached_interface.minimum_height <= 1))) set_minimum_width (a_minimum_width: INTEGER_32) -- Set the minimum horizontal size to a_minimum_width in pixels. -- (from EV_WIDGET_I) require -- from EV_WIDGET_I a_minimum_width_positive: a_minimum_width >= 0 ensure -- from EV_WIDGET_I minimum_width_assigned: is_usable implies ((a_minimum_width > 0 implies attached_interface.minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (attached_interface.minimum_width <= 1))) set_background_pixmap (a_pixmap: EV_PIXMAP) -- Assign a_pixmap to pixmap. -- (from EV_PIXMAPABLE_I) require -- from EV_PIXMAPABLE_I pixmap_not_void: a_pixmap /= Void set_tooltip (a_tooltip: READABLE_STRING_GENERAL) -- Assign a_tooltip to Current. require -- from EV_TOOLTIPABLE_I a_tooltip_not_void: a_tooltip /= Void feature -- Removal clear -- Remove all items from Current. ensure to_implement_assertion ("EV_GRID_I.clear - All items positions return `Void'.") remove_column (a_column: INTEGER_32) -- Remove column a_column. require a_column_positive: a_column > 0 a_column_less_than_column_count: a_column <= column_count 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 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 node_counts_correct_in_parent: attached (old row_internal (a_row).parent_row_i) as l_parent_row_i implies l_parent_row_i.node_counts_correct 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 valid_lower_index: lower_index >= 1 and lower_index <= row_count valid_upper_index: upper_index >= lower_index and upper_index <= row_count 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") wipe_out -- Remove all columns and rows from Current. ensure columns_removed: column_count = 0 rows_removed: row_count = 0 feature -- Duplication copy (other: EV_GRID_I) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other frozen deep_copy (other: EV_GRID_I) -- 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_I -- 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_I) -- 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_I -- 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_I -- 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 close_dockable_dialog (dockable_dialog: EV_DOCKABLE_DIALOG) -- Close request received by dockable_dialog so -- restore widget contained back to its original position -- in its old parent if possible. -- We must fire dock_ended actions. -- (from EV_DOCKABLE_SOURCE_I) ensure -- from EV_DOCKABLE_SOURCE_I dockable_dialog_destroyed: dockable_dialog.is_destroyed complete_dock -- Complete a dock from `source_being_docked`. -- (from EV_DOCKABLE_SOURCE_I) require -- from EV_DOCKABLE_SOURCE_I source_being_docked: source_being_docked /= Void ensure -- from EV_DOCKABLE_SOURCE_I not_dock_executing: not is_dock_executing insert_separator_not_parented: Insert_sep.parent = Void insert_label_not_parented: Insert_label.parent = Void frozen default: detachable EV_GRID_I -- 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 propagate_background_color -- Propagate the current background color of the -- container to the children. -- (from EV_CONTAINER_I) ensure -- from EV_CONTAINER_I background_color_propagated: attached_interface.cell_background_color_propagated propagate_foreground_color -- Propagate the current foreground color of the -- container to the children. -- (from EV_CONTAINER_I) ensure -- from EV_CONTAINER_I foreground_color_propagated: attached_interface.cell_foreground_color_propagated refresh_now -- Force an immediate redraw of Current. -- (from EV_WIDGET_I) feature -- Inapplicable Drag_cursor: EV_POINTER_STYLE -- Cursor used when Current is being transported. -- (from EV_DOCKABLE_SOURCE_I) feature -- Implementation key_press_received (a_key: EV_KEY) -- Called by `key_press_actions` of `drawable`. feature disable_horizontal_offset_set_to_zero_when_items_smaller_than_viewable_width -- Ensure `is_horizontal_offset_set_to_zero_when_items_smaller_than_viewable_width` is False ensure set: not is_horizontal_offset_set_to_zero_when_items_smaller_than_viewable_width is_horizontal_offset_set_to_zero_when_items_smaller_than_viewable_width: BOOLEAN -- This is required for cases where you have two grids, one acting as a header for another. -- If the vertical scroll bar of one is displayed, and the simulated header does not have -- scroll bars displayed, then the virtual positions permitted are not in synch and we wish -- to turn off the automatic scrolling of the header grid as it should always change in synch -- with the main grid. This should probably be moved into the interface of EV_GRID at some point. recompute_horizontal_scroll_bar -- Recompute horizontal scroll bar positioning. feature -- Access EV_DRAGABLE_SOURCE. dockable_dialog_target: detachable EV_DOCKABLE_DIALOG -- A dockable dialog that will be created as -- necessary. This is not a local, to avoid it -- being garbage collected. -- (from EV_SHARED_TRANSPORT_I) Global_drag_targets: ARRAYED_LIST [INTEGER_32] -- Shortcut to EV_APPLICATION.pnd_targets. -- (from EV_SHARED_TRANSPORT_I) frozen Insert_label: EV_CELL -- Label used to indicate where Current will be placed in target. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I result_not_void: Result /= Void Insert_label_imp: EV_CELL_I -- Once access to implementation of `insert_label`. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I Result /= Void Insert_sep: EV_TOOL_BAR_SEPARATOR -- Once access to a separator used to indicate the insertion position -- when moving tool bar items. -- (from EV_SHARED_TRANSPORT_I) Insert_sep_imp: EV_TOOL_BAR_SEPARATOR_I -- Once access to implementation of `insert_sep`. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I Result /= Void Internal_screen: EV_SCREEN -- Once access to an EV_SCREEN. -- (from EV_SHARED_TRANSPORT_I) original_x_offset: INTEGER_16 -- Original x_offset and original_y_offset of transport -- realtive to widget. Only used for dragable transports. -- (from EV_SHARED_TRANSPORT_I) original_y_offset: INTEGER_16 -- Original x_offset and original_y_offset of transport -- realtive to widget. Only used for dragable transports. -- (from EV_SHARED_TRANSPORT_I) originating_source: detachable EV_DOCKABLE_SOURCE_I -- Dragable source that originated the transport of source_being_dragged. -- (from EV_SHARED_TRANSPORT_I) remove_insert_label -- Remove `insert_label` from its current `parent`. -- We must handle a special case for cells. If the parent is a cell, -- then we remove the cell from its parent, and then restore it. -- Otherwise, when the label, removed, the cell keeps it size, and cells -- are normally used with `real_target` when the cell must -- not be visible. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I not_parented: Insert_label.parent = Void remove_insert_sep -- Ensure inset_sep is not parented. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I not_parented: Insert_sep.parent = Void source_being_docked: detachable EV_DOCKABLE_SOURCE_I -- Dragable source currently being transported. May be a -- WIDGET_IMP or an EV_TOOL_BAR_BUTTON_IMP. -- (from EV_SHARED_TRANSPORT_I) feature -- Access EV_PICK_AND_DROPABLE. Default_accept_cursor: EV_POINTER_STYLE -- Used in lieu of a user defined `accept_cursor`. -- (from EV_SHARED_TRANSPORT_I) Default_deny_cursor: EV_POINTER_STYLE -- Used in lieu of a user defined `deny_cursor`. -- (from EV_SHARED_TRANSPORT_I) Default_pixmaps: EV_STOCK_PIXMAPS -- Default pixmaps -- (from EV_SHARED_TRANSPORT_I) Global_pnd_targets: HASH_TABLE [INTEGER_32, INTEGER_32] -- Shortcut to EV_APPLICATION.pnd_targets. -- (from EV_SHARED_TRANSPORT_I) rubber_band_is_drawn: BOOLEAN -- Is a rubber band line currently on the screen? -- (from EV_SHARED_TRANSPORT_I) feature -- Access common. pointer_x: INTEGER_16 -- (from EV_SHARED_TRANSPORT_I) pointer_y: INTEGER_16 -- (from EV_SHARED_TRANSPORT_I) feature -- Event handling column_deselect_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_COLUMN] -- Actions to be performed when a column is deselected. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES_I not_void: Result /= Void dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when `pebble` is picked up. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES_I) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES_I not_void: Result /= Void docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE -- Actions to be performed -- (from EV_DOCKABLE_TARGET_ACTION_SEQUENCES_I) ensure -- from EV_DOCKABLE_TARGET_ACTION_SEQUENCES_I not_void: Result /= Void dpi_changed_actions: EV_DPI_ACTION_SEQUENCE -- Actions to be performed when dpi changes. -- (from EV_WIDGET_ACTION_SEQUENCES_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I not_void: Result /= Void file_drop_actions: EV_LITE_ACTION_SEQUENCE [LIST [STRING_32]] -- Actions to be performed when an OS file drop occurs on Current. -- (from EV_WIDGET_ACTION_SEQUENCES_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I not_void: Result /= Void focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is gained. -- (from EV_WIDGET_ACTION_SEQUENCES_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I not_void: Result /= Void item_activate_actions: EV_LITE_ACTION_SEQUENCE [EV_GRID_ITEM, EV_POPUP_WINDOW] -- Actions to be performed to setup an item that is currently activated. -- Overrides default setup of activatable items. -- Arguments of TUPLE (with names for clarity): -- -- activate_item: EV_GRID_ITEM -- The item that is currently activated. -- popup_window: EV_WINDOW -- The popup window used to interactively edit `activate_item`, window has already been sized and positioned. -- (from EV_GRID_ACTION_SEQUENCES_I) item_deactivate_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item is deactivated. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_not_void: Result /= Void item_deselect_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item is deselected. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I 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 here. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I not_void: Result /= Void item_select_actions: EV_GRID_ITEM_ACTION_SEQUENCE -- Actions to be performed when an item is selected. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I not_void: Result /= Void new_item_actions: EV_NEW_ITEM_ACTION_SEQUENCE -- Actions to be performed when a new item is added. -- (from EV_CONTAINER_ACTION_SEQUENCES_I) ensure -- from EV_CONTAINER_ACTION_SEQUENCES_I 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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I not_void: Result /= Void 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_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_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_not_void: Result /= Void 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I not_void: Result /= Void resize_actions: EV_GEOMETRY_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES_I) ensure -- from EV_WIDGET_ACTION_SEQUENCES_I not_void: Result /= Void row_collapse_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is collapsed. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I 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_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_not_void: Result /= Void row_select_actions: EV_GRID_ROW_ACTION_SEQUENCE -- Actions to be performed when a row is selected. -- (from EV_GRID_ACTION_SEQUENCES_I) ensure -- from EV_GRID_ACTION_SEQUENCES_I result_not_void: Result /= Void 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_I) 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_I) 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. 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`. row_count: INTEGER_32 -- Number of rows in Current. 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. 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 -- Pick and Drop are_column_separators_enabled: BOOLEAN -- Is a vertical separator displayed in color `separator_color` after each column? are_row_separators_enabled: BOOLEAN -- Is a horizontal separator displayed in color `separator_color` after each row? drop_action_intermediary (a_pebble: ANY) -- A PND drop has occurred on a grid item. item_accept_cursor_function: detachable FUNCTION [EV_GRID_ITEM, EV_POINTER_STYLE] -- Function used to retrieve the PND accept cursor for a particular item. item_accepts_pebble (a_item: detachable EV_GRID_ITEM; a_pebble: ANY): BOOLEAN -- Do any actions accept a_pebble for a_item. require a_pebble_not_void: a_pebble /= 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. item_target: detachable EV_GRID_ITEM -- Item currently at pointer position. item_veto_pebble_function: detachable FUNCTION [EV_GRID_ITEM, ANY, BOOLEAN] -- User item veto function. separator_color: EV_COLOR -- Color used to display column and row separators. set_accept_cursor (a_cursor: like accept_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. set_deny_cursor (a_cursor: like deny_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that doesn't accept `pebble` during pick and drop. set_item_accept_cursor_function (a_function: like item_accept_cursor_function) -- Assign a_function to `item_accept_cursor_function`. ensure item_accept_cursor_function_set: item_accept_cursor_function = a_function set_item_deny_cursor_function (a_function: like item_deny_cursor_function) -- Assign a_function to `item_deny_cursor_function`. 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]) -- Set a_function to compute `pebble`. -- 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. -- To handle this data use a_function of type -- FUNCTION [ANY, TUPLE [EV_GRID_ITEM], ANY] and return the -- pebble as a function of EV_GRID_ITEM. set_item_veto_pebble_function (a_function: like item_veto_pebble_function) -- Assign a_function to `item_veto_pebble_function`. ensure item_veto_pebble_function_set: item_veto_pebble_function = a_function user_pebble_function_intermediary (a_x, a_y: INTEGER_32): detachable ANY -- Intermediary function used for grid item pick and drop. user_pebble_function_intermediary_locked (a_x, a_y: INTEGER_32; locked: EV_GRID_LOCKED_I): detachable ANY -- Intermediary function used for grid item pick and drop on the widgets comprising the locked columns and rows. veto_pebble_function_intermediary (a_pebble: ANY): BOOLEAN -- Intermediary function used for pebble vetoing. 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_displayed: BOOLEAN -- Is Current visible on the screen? -- False if Current is entirely obscured by another window. -- (from EV_WIDGET_I) is_show_requested: BOOLEAN -- Will Current be displayed when its parent is? -- See also `is_displayed`. -- (from EV_WIDGET_I) invariant drawer_not_void: is_initialized implies drawer /= Void drawable_not_void: is_initialized implies drawable /= Void header_positioned_corrently: is_initialized implies header_viewport.x_offset >= 0 and header_viewport.y_offset = 0 internal_client_y_valid_while_vertical_scrollbar_hidden: is_initialized and then is_vertical_scroll_bar_show_requested and then not internal_vertical_scroll_bar.is_show_requested implies internal_client_y = 0 internal_client_y_valid_while_vertical_scrollbar_shown: is_initialized and then internal_vertical_scroll_bar.is_show_requested implies internal_client_y >= 0 internal_client_x_valid_while_horizontal_scrollbar_hidden: is_initialized and then is_horizontal_scroll_bar_show_requested and then not internal_horizontal_scroll_bar.is_show_requested implies internal_client_x = 0 internal_client_x_valid_while_horizontal_scrollbar_shown: is_initialized and then internal_horizontal_scroll_bar.is_show_requested implies internal_client_x >= 0 row_heights_fixed_implies_row_offsets_void: is_initialized and then not uses_row_offsets implies row_offsets = Void row_lists_count_equal: is_initialized implies internal_row_data.count = rows.count displayed_column_count_not_greater_than_column_count: is_initialized implies displayed_column_count <= column_count computed_visible_row_count_equals_row_when_not_users_row_offsets: is_initialized and then not uses_row_offsets implies visible_row_count = row_count computed_visible_row_count_no_greater_than_rows: is_initialized implies visible_row_count <= row_count tree_disabled_implies_visible_rows_equal_hidden_rows: (is_initialized and then not is_tree_enabled and not vertical_computation_required) implies row_count - non_displayed_row_count = visible_row_count internal_viewport_positions_equal_to_viewports: is_initialized implies (viewport.x_offset = viewport_x_offset and viewport.y_offset = viewport_y_offset) tree_node_connector_color_not_void: is_initialized implies tree_node_connector_color /= Void -- from EV_WIDGET_I is_displayed_implies_show_requested: is_usable and is_displayed implies is_show_requested -- from EV_PICK_AND_DROPABLE_I 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 pebble_function_takes_two_integer_open_operands: attached pebble_function as l_pebble_function implies l_pebble_function.valid_operands ([1, 1]) -- from EV_ANY_I interface_coupled: is_usable implies interface /= Void and then attached_interface.implementation = Current base_make_called: is_usable implies base_make_called -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from EV_POSITIONED_I minimum_width_positive_or_zero: is_usable implies minimum_width >= 0 minimum_height_positive_or_zero: is_usable implies minimum_height >= 0 -- from EV_DOCKABLE_SOURCE_I widget_or_item_source: not (widget_source_being_docked /= Void and item_source_being_docked /= Void) dock_executing: is_dock_executing implies widget_source_being_docked /= Void or item_source_being_docked /= Void note copyright: "Copyright (c) 1984-2021, 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_I -- Generated by Eiffel Studio --
For more details: eiffel.org