Automatic generation produced by ISE Eiffel
note description: "[ Multi-column lists that allow in-place editing of list row items. By default ALLcolumns are editable. Only one single column item is editable at any time and the widget typewhich can be edited must conform to EV_TEXTABLE. ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2023-11-21 03:48:49 -0900 (Tue, 21 Nov 2023) $" revision: "$Revision: 107415 $" class interface EV_EDITABLE_LIST create make (a_window: EV_WINDOW) -- Create list with all columns editable and with relative 'a_window'. require window_not_void: a_window /= Void feature -- Access accept_cursor: EV_POINTER_STYLE -- Result is cursor displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE result_not_void: Result /= Void ensure then -- from EV_PICK_AND_DROPABLE cursor_valid: (attached implementation.accept_cursor implies Result = implementation.accept_cursor) or else Result = Default_pixmaps.Standard_cursor actual_drop_target_agent: detachable FUNCTION [INTEGER_32, INTEGER_32, detachable EV_ABSTRACT_PICK_AND_DROPABLE] -- Overrides default drop target on a certain position. -- If Void, Current will use the default drop target. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.actual_drop_target_agent at alias "@" (i: INTEGER_32): like item assign dl_put_i_th -- Item at i-th position -- Was declared in {CHAIN} as synonym of `i_th`. -- (from CHAIN) require -- from TABLE valid_key: valid_index (i) background_color: EV_COLOR -- Color displayed behind foreground features. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed ensure -- from EV_COLORIZABLE bridge_ok: Result.is_equal (implementation.background_color) column_count: INTEGER_32 -- Column count. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.column_count configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY] -- Agent used for customizing the Pick and Drop Target Menu of Current. -- (from EV_PICK_AND_DROPABLE) cursor: EV_DYNAMIC_LIST_CURSOR [EV_MULTI_COLUMN_LIST_ROW] -- Current cursor position. -- (from EV_DYNAMIC_LIST) require -- from CURSOR_STRUCTURE True ensure -- from CURSOR_STRUCTURE cursor_not_void: Result /= Void ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result.is_equal (implementation.cursor) data: detachable ANY -- Arbitrary user data may be stored here. -- (from EV_ANY) default_identifier_name: STRING_32 -- Default name if no other name is set. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_key_processing_handler: detachable PREDICATE [EV_KEY] assign set_default_key_processing_handler -- Agent used to determine whether the default key processing should occur for Current. -- If agent returns True then default key processing continues as normal, False prevents -- default key processing from occurring. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.default_key_processing_handler deny_cursor: EV_POINTER_STYLE -- Result is cursor displayed when the screen pointer is over a -- target that does not accept `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE result_not_void: Result /= Void ensure then -- from EV_PICK_AND_DROPABLE cursor_valid: (attached implementation.deny_cursor implies Result = implementation.deny_cursor) or else Result = Default_pixmaps.No_cursor first: like item -- Item at first position -- (from CHAIN) require -- from CHAIN not_empty: not is_empty foreground_color: EV_COLOR -- Color of foreground features like text. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed ensure -- from EV_COLORIZABLE bridge_ok: Result.is_equal (implementation.foreground_color) full_identifier_path: STRING_32 -- Full name of object by prepending path of parent -- Uses '.' as a separator. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_correct: parent = Void implies Result.is_equal (identifier_name) result_correct: attached parent as l_parent implies Result.is_equal (l_parent.full_identifier_path + ".".as_string_32 + identifier_name) generating_type: TYPE [detachable EV_EDITABLE_LIST] -- 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 item): BOOLEAN -- Does chain include v? -- (Reference or object equality, -- based on `object_comparison`.) -- (from CHAIN) require -- from CONTAINER True ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty help_context: detachable FUNCTION [EV_HELP_CONTEXT] -- Agent that evaluates to help context sent to help engine when help is requested -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed ensure -- from EV_HELP_CONTEXTABLE bridge_ok: Result = implementation.help_context i_th alias "[]" (i: INTEGER_32): like item -- Item at i-th position. -- (from EV_DYNAMIC_LIST) require -- from TABLE valid_key: valid_index (i) require -- from READABLE_INDEXABLE valid_index: valid_index (i) ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result.is_equal (implementation.i_th (i)) frozen id_object (an_id: INTEGER_32): detachable IDENTIFIED -- Object associated with an_id (void if no such object) -- (from IDENTIFIED) ensure -- from IDENTIFIED consistent: Result = Void or else Result.object_id = an_id identifier_name: STRING_32 -- Name of object -- If no specific name is set, `default_identifier_name` is used. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name) index: INTEGER_32 -- Current position. -- (from EV_DYNAMIC_LIST) require -- from LINEAR True ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result = implementation.index index_of (v: like item; i: INTEGER_32): INTEGER_32 -- Index of ith occurrence of v. -- (from EV_DYNAMIC_LIST) require -- from LINEAR positive_occurrences: i > 0 ensure -- from LINEAR non_negative_result: Result >= 0 ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result = implementation.index_of (v, i) item: EV_MULTI_COLUMN_LIST_ROW -- Item at current position. -- (from EV_DYNAMIC_LIST) require -- from ACTIVE readable: readable require -- from TRAVERSABLE not_off: not off ensure then -- from EV_DYNAMIC_LIST not_void: Result /= Void bridge_ok: Result.is_equal (implementation.item) item_for_iteration: EV_MULTI_COLUMN_LIST_ROW -- Item at current position -- (from LINEAR) require -- from LINEAR not_off: not off last: like item -- Item at last position -- (from CHAIN) require -- from CHAIN not_empty: not is_empty new_cursor: INDEXABLE_ITERATION_CURSOR [EV_MULTI_COLUMN_LIST_ROW] -- Fresh cursor associated with current structure -- (from READABLE_INDEXABLE) require -- from ITERABLE True ensure -- from ITERABLE result_attached: Result /= Void frozen object_id: INTEGER_32 -- Unique for current object in any given session -- (from IDENTIFIED) ensure -- from IDENTIFIED valid_id: Result > 0 implies id_object (Result) = Current parent: detachable EV_CONTAINER -- Contains Current. -- (from EV_WIDGET) require -- from EV_IDENTIFIABLE not_destroyed: not is_destroyed ensure -- from EV_IDENTIFIABLE correct: has_parent implies Result /= Void correct: not has_parent implies Result = Void ensure then -- from EV_WIDGET bridge_ok: Result = implementation.parent pebble: detachable ANY -- Data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble pebble_function: detachable FUNCTION [detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_function pebble_positioning_enabled: BOOLEAN -- If True then pick and drop start coordinates are -- `pebble_x_position`, `pebble_y_position`. -- If False then pick and drop start coordinates are -- the pointer coordinates. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_positioning_enabled pebble_x_position: INTEGER_32 -- Initial x position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_x_position pebble_y_position: INTEGER_32 -- Initial y position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_y_position pixmaps_height: INTEGER_32 -- Height of displayed pixmaps in the list. -- (from EV_ITEM_PIXMAP_SCALER) require -- from EV_ITEM_PIXMAP_SCALER not_destroyed: not is_destroyed ensure -- from EV_ITEM_PIXMAP_SCALER bridge_ok: Result = implementation.pixmaps_height pixmaps_width: INTEGER_32 -- Width of displayed pixmaps in the list. -- (from EV_ITEM_PIXMAP_SCALER) require -- from EV_ITEM_PIXMAP_SCALER not_destroyed: not is_destroyed ensure -- from EV_ITEM_PIXMAP_SCALER bridge_ok: Result = implementation.pixmaps_width pointer_position: EV_COORDINATE -- Position of the screen pointer relative to Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_show_requested: is_show_requested pointer_style: EV_POINTER_STYLE -- Cursor displayed when pointer is over this widget. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed real_target: detachable EV_DOCKABLE_TARGET -- Result is target used during a dockable transport if -- mouse pointer is above Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.real_target retrieve_item_by_data (some_data: ANY; should_compare_objects: BOOLEAN): detachable EV_MULTI_COLUMN_LIST_ROW -- Result is first item in Current with data -- matching some_data. Compare objects if -- should_compare_objects otherwise compare references. -- (from EV_DYNAMIC_LIST) ensure -- from EV_DYNAMIC_LIST not_found_in_empty: Result /= Void implies not is_empty index_not_changed: old index = index retrieve_items_by_data (some_data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_MULTI_COLUMN_LIST_ROW] -- Result is all items in Current with data -- matching some_data. Compare objects if -- should_compare_objects otherwise compare references. -- (from EV_DYNAMIC_LIST) ensure -- from EV_DYNAMIC_LIST result_not_void: Result /= Void not_found_in_empty: not Result.is_empty implies not is_empty index_not_changed: old index = index row_height: INTEGER_32 -- Height in pixels of each row. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.row_height selected_item: detachable like item -- Currently selected item. -- Topmost selected item if multiple items are selected. -- (For multiple selections see `selected_items`). -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.selected_item selected_items: DYNAMIC_LIST [like item] -- Currently selected items. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: lists_equal (Result, implementation.selected_items) target_data_function: detachable FUNCTION [like pebble, EV_PND_TARGET_DATA] -- Function for computing target meta data based on source pebble. -- Primarily used for Pick and Drop target menu. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) note option: stable target_name: detachable READABLE_STRING_GENERAL -- Optional textual name describing Current pick and drop hole. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) note option: stable tooltip: STRING_32 -- Tooltip displayed on Current. -- If Result is empty then no tooltip displayed. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed ensure -- from EV_TOOLTIPABLE bridge_ok: is_bridge_ok (Result) not_void: Result /= Void cloned: is_cloned (Result) feature -- Measurement count: INTEGER_32 -- Number of items. -- (from EV_DYNAMIC_LIST) require -- from FINITE True require -- from READABLE_INDEXABLE True ensure -- from FINITE count_non_negative: Result >= 0 ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result = implementation.count dpi: NATURAL_32 -- Window dpi -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED positive_or_zero: Result >= 0 height: INTEGER_32 -- Vertical size in pixels. -- Same as `minimum_height` when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.height Lower: INTEGER_32 = 1 -- Minimum index. -- (from CHAIN) minimum_height: INTEGER_32 -- Lower bound on `height` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_height positive_or_zero: Result >= 0 minimum_width: INTEGER_32 -- Lower bound on `width` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_width positive_or_zero: Result >= 0 occurrences (v: like item): INTEGER_32 -- Number of times v appears. -- (Reference or object equality, -- based on `object_comparison`.) -- (from CHAIN) require -- from BAG True require -- from LINEAR True ensure -- from BAG non_negative_occurrences: Result >= 0 screen_x: INTEGER_32 -- Horizontal offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_x screen_y: INTEGER_32 -- Vertical offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_y width: INTEGER_32 -- Horizontal size in pixels. -- Same as `minimum_width` when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.width x_position: INTEGER_32 -- Horizontal offset relative to parent `x_position` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.x_position y_position: INTEGER_32 -- Vertical offset relative to parent `y_position` in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.y_position feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal alias "≡≡≡" (other: EV_EDITABLE_LIST): 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_EDITABLE_LIST): BOOLEAN -- Does other contain the same elements? -- (from LIST) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from LIST indices_unchanged: index = old index and other.index = old other.index true_implies_same_size: Result implies count = other.count 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_EDITABLE_LIST): 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 after: BOOLEAN -- Is there no valid cursor position to the right of cursor? -- (from LIST) require -- from LINEAR True all_columns_editable: BOOLEAN -- Are all columns in the list editable? all_rows_editable: BOOLEAN -- Are all rows in the list editable? before: BOOLEAN -- Is there no valid cursor position to the left of cursor? -- (from LIST) require -- from BILINEAR True column_alignment (a_column: INTEGER_32): EV_TEXT_ALIGNMENT -- Result is alignment of column a_column. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column >= 1 and a_column <= column_count ensure -- from EV_MULTI_COLUMN_LIST result_not_void: Result /= Void bridge_ok: Result.is_equal (implementation.column_alignment (a_column)) column_editable (i: INTEGER_32): BOOLEAN -- Is column at index 'i' allowed to be edited? column_title (a_column: INTEGER_32): STRING_32 -- Title of a_column. -- Returns "" if no title given yet. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_positive: a_column >= 1 ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result.is_equal (implementation.column_title (a_column)) cloned: Result /= implementation.column_title (a_column) column_width (a_column: INTEGER_32): INTEGER_32 -- Width of a_column in pixels. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column >= 1 and a_column <= column_count ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.column_width (a_column) 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 debug_output: STRING_32 -- String that should be displayed in debugger to represent Current. -- (from EV_IDENTIFIABLE) ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void exhausted: BOOLEAN -- Has structure been completely explored? -- (from LINEAR) ensure -- from LINEAR exhausted_when_off: off implies Result extendible: BOOLEAN -- May new items be added? (Answer: yes.) -- (from DYNAMIC_CHAIN) require -- from COLLECTION True Full: BOOLEAN = False -- Is structured filled to capacity? (Answer: no.) -- (from EV_DYNAMIC_LIST) has_capture: BOOLEAN -- Does widget have capture? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_capture has_focus: BOOLEAN -- Does widget have the keyboard focus? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_focus has_identifier_name_set: BOOLEAN -- Is a specific identifier name set? -- (from EV_IDENTIFIABLE) has_parent: BOOLEAN -- Does identifiable has a parent? -- (from EV_IDENTIFIABLE) frozen id_freed: BOOLEAN -- Has Current been removed from the table? -- (from IDENTIFIED) is_displayed: BOOLEAN -- Is Current visible on the screen? -- True when show requested and parent displayed. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.is_displayed is_dockable: BOOLEAN -- Is Current dockable? -- If True, then Current may be dragged -- from its current parent. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_dockable is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) require -- from CONTAINER True is_external_docking_enabled: BOOLEAN -- Is Current able to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport? -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_enabled is_external_docking_relative: BOOLEAN -- Will dockable dialog displayed when Current is docked externally -- be displayed relative to parent window of Current? -- Otherwise displayed as a standard window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_relative is_in_default_state_for_tabs: BOOLEAN -- Default state for widgets. -- (from EV_TAB_CONTROLABLE) is_inserted (v: EV_MULTI_COLUMN_LIST_ROW): BOOLEAN -- Has v been inserted by the most recent insertion? -- (By default, the value returned is equivalent to calling -- has (v). However, descendants might be able to provide more -- efficient implementations.) -- (from COLLECTION) is_sensitive: BOOLEAN -- Is object sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE bridge_ok: Result = implementation.user_is_sensitive is_show_requested: BOOLEAN -- Will Current be displayed when its parent is? -- See also `is_displayed`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.is_show_requested is_tabable_from: BOOLEAN -- Is Current able to be tabbed from? -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed is_tabable_to: BOOLEAN -- Is Current able to be tabbed to? -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed isfirst: BOOLEAN -- Is cursor at first position? -- (from CHAIN) ensure -- from CHAIN valid_position: Result implies not is_empty islast: BOOLEAN -- Is cursor at last position? -- (from CHAIN) ensure -- from CHAIN valid_position: Result implies not is_empty mode_is_configurable_target_menu: BOOLEAN -- Is the user interface mode a configurable pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_configurable_target_menu mode_is_drag_and_drop: BOOLEAN -- Is the user interface mode drag and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_drag_and_drop mode_is_pick_and_drop: BOOLEAN -- Is the user interface mode pick and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_pick_and_drop mode_is_target_menu: BOOLEAN -- Is the user interface mode a pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_target_menu multiple_selection_enabled: BOOLEAN -- Can more than one item be selected? -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.multiple_selection_enabled object_comparison: BOOLEAN -- Must search operations use `equal` rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) off: BOOLEAN -- Is there no current item? -- (from CHAIN) require -- from TRAVERSABLE True prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from DYNAMIC_TABLE) require -- from COLLECTION True readable: BOOLEAN -- Is there a current item that may be read? -- (from SEQUENCE) require -- from ACTIVE True real_source: detachable EV_DOCKABLE_SOURCE -- Result is source to be dragged -- when a docking drag occurs on Current. -- If Void, Current is dragged. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.real_source replaceable: BOOLEAN -- Can current item be replaced? -- (from ACTIVE) row_editable (i: INTEGER_32): BOOLEAN -- Is row at index 'i' allowed to be edited? 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)) set_pixmaps_size (a_width: INTEGER_32; a_height: INTEGER_32) -- Set size of pixmaps disaplyed in Current. -- Note: Default value is 16x16 -- (from EV_ITEM_PIXMAP_SCALER) require -- from EV_ITEM_PIXMAP_SCALER not_destroyed: not is_destroyed valid_width: a_width > 0 valid_height: a_height > 0 ensure -- from EV_ITEM_PIXMAP_SCALER width_set: pixmaps_width = a_width height_set: pixmaps_height = a_height title_shown: BOOLEAN -- Is a row displaying column titles shown? -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST bridge_ok: Result = implementation.title_shown valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? -- This is True if p conforms to EV_DYNAMIC_LIST_CURSOR and -- if it points to an item, Current must have it. -- (from EV_DYNAMIC_LIST) require -- from CURSOR_STRUCTURE True ensure then -- from EV_DYNAMIC_LIST bridge_ok: Result = implementation.valid_cursor (p) valid_cursor_index (i: INTEGER_32): BOOLEAN -- Is i correctly bounded for cursor movement? -- (from CHAIN) ensure -- from CHAIN valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1)) valid_index (i: INTEGER_32): BOOLEAN -- Is i within allowable bounds? -- (from CHAIN) require -- from READABLE_INDEXABLE True require -- from TABLE True ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= count) ensure then -- from CHAIN valid_index_definition: Result = ((i >= 1) and (i <= count)) writable: BOOLEAN -- Is there a current item that may be modified? -- (from SEQUENCE) require -- from ACTIVE True feature -- Status setting align_text_center (a_column: INTEGER_32) -- Display text of a_column centered. -- First column is always left aligned. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 1 and a_column <= column_count ensure -- from EV_MULTI_COLUMN_LIST center_aligned: column_alignment (a_column).is_center_aligned align_text_left (a_column: INTEGER_32) -- Display text of a_column left aligned. -- First column is always left aligned. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 1 and a_column <= column_count ensure -- from EV_MULTI_COLUMN_LIST left_aligned: column_alignment (a_column).is_left_aligned align_text_right (a_column: INTEGER_32) -- Display text of a_column right aligned. -- First column is always left aligned. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 1 and a_column <= column_count ensure -- from EV_MULTI_COLUMN_LIST right_aligned: column_alignment (a_column).is_right_aligned center_pointer -- Position screen pointer over center of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed change_widget_type (i: INTEGER_32; a_widget: EV_TEXTABLE) -- Set widget type to be displayed at column index 'i' require editable_column: column_editable (i) compare_objects -- Ensure that future search operations will use `equal` -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than `equal` for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison disable_capture -- Disable grab of all user input events. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET not_has_capture: not has_capture disable_dockable -- Ensure Current is not dockable. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE not_is_dockable: not is_dockable disable_external_docking -- Assign False to `is_external_docking_enabled`. -- Forbid Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE not_externally_dockable: not is_external_docking_enabled disable_external_docking_relative -- Assign False to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed as a standard window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE external_docking_not_relative: not is_external_docking_relative disable_multiple_selection -- Allow only one item to be selected. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST not_multiple_selection_enabled: not multiple_selection_enabled disable_pebble_positioning -- Assign False to `pebble_positioning_enabled`. -- The pick and drop will start at the pointer position. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_positioning_updated: not pebble_positioning_enabled disable_sensitive -- Make object non-sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE is_unsensitive: not is_sensitive disable_tabable_from -- Make `is_tabable_from` False. -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed ensure -- from EV_TAB_CONTROLABLE not_is_tabable_from: not is_tabable_from disable_tabable_to -- Make `is_tabable_to` False. -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed ensure -- from EV_TAB_CONTROLABLE not_is_tabable_to: not is_tabable_to enable_capture -- Grab all user input events (mouse and keyboard). -- `disable_capture` must be called to resume normal input handling. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_displayed: is_displayed ensure -- from EV_WIDGET has_capture: has_capture enable_dockable -- Ensure Current is dockable. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE is_dockable: is_dockable enable_external_docking -- Assign True to `is_external_docking_enabled`. -- Allows Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE is_externally_dockable: is_external_docking_enabled enable_external_docking_relative -- Assign True to `is_external_docking_relative`, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed relative to the top level window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE external_docking_not_relative: is_external_docking_relative enable_multiple_selection -- Allow more than one item to be selected. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST multiple_selection_enabled: multiple_selection_enabled enable_pebble_positioning -- Assign True to `pebble_positioning_enabled`. -- Use `pebble_x_position` and `pebble_y_position` as the initial coordinates -- for the pick and drop in pixels relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_positioning_updated: pebble_positioning_enabled enable_sensitive -- Make object sensitive to user input. -- (from EV_SENSITIVE) require -- from EV_SENSITIVE not_destroyed: not is_destroyed ensure -- from EV_SENSITIVE is_sensitive: (parent = Void or parent_is_sensitive) implies is_sensitive enable_tabable_from -- Make `is_tabable_from` True. -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed ensure -- from EV_TAB_CONTROLABLE is_tabable_from: is_tabable_from enable_tabable_to -- Make `is_tabable_to` True. -- (from EV_TAB_CONTROLABLE) require -- from EV_TAB_CONTROLABLE not_destroyed: not is_destroyed ensure -- from EV_TAB_CONTROLABLE is_tabable_to: is_tabable_to ensure_item_visible (an_item: EV_MULTI_COLUMN_LIST_ROW) -- Ensure an_item is visible in Current. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed is_displayed: is_displayed an_item_contained: has (an_item) hide -- Request that Current not be displayed even when its parent is. -- If successful, make `is_show_requested` False. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed hide_title_row -- Hide row displaying column titles. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST not_title_shown: not title_shown remove_default_key_processing_handler -- Ensure `default_key_processing_handler` is Void. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed remove_pebble -- Make `pebble` Void and `pebble_function` `Void, -- Removing transport. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_removed: pebble = Void and pebble_function = Void remove_real_source -- Ensure `real_source` is Void. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE real_source_void: real_source = Void remove_real_target -- Ensure `real_target` is Void. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET real_target_void: real_target = Void remove_selection -- Ensure that `selected_items` is empty. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST selected_items_empty: selected_items.is_empty set_accept_cursor (a_cursor: detachable like accept_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE accept_cursor_assigned: attached a_cursor as l_accept_cursor implies l_accept_cursor ~ accept_cursor set_actual_drop_target_agent (an_agent: like actual_drop_target_agent) -- Assign an_agent to `actual_drop_target_agent`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed an_agent_not_void: an_agent /= Void ensure -- from EV_WIDGET assigned: actual_drop_target_agent = an_agent set_all_columns_editable -- Make every column editable. require has_columns: column_count > 0 set_all_rows_editable -- Make every row editable. set_column_editable (a_flag: BOOLEAN; i: INTEGER_32) -- Make column at index 'i' editable according to 'a_flag'. set_configurable_target_menu_handler (a_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY]) -- Set Configurable Target Menu Handler to a_handler. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_PICK_AND_DROPABLE configurable_target_menu_hander_assigned: configurable_target_menu_handler = a_handler set_configurable_target_menu_mode -- Set user interface mode to pop-up menu of targets. -- Target menu is configurable as the first option can be used to -- initiate a regular 'pick and drop' of the source pebble. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE target_menu_mode_set: mode_is_configurable_target_menu set_default_colors -- Set foreground and background color to their default values. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed set_default_key_processing_handler (a_handler: like default_key_processing_handler) -- Assign `default_key_processing_handler` to a_handler. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed set_deny_cursor (a_cursor: detachable like deny_cursor) -- Set a_cursor to be displayed when the screen pointer is not -- over a valid target. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE deny_cursor_assigned: attached a_cursor as l_deny_cursor implies l_deny_cursor ~ deny_cursor set_drag_and_drop_mode -- Set user interface mode to drag and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE drag_and_drop_set: mode_is_drag_and_drop set_focus -- Grab keyboard focus if `is_displayed`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed is_sensitive: is_sensitive set_non_empty_column_values (a_flag: BOOLEAN) -- Set so edited column values are not allowed to be empty. set_pebble (a_pebble: ANY) -- Assign a_pebble to `pebble`. -- Overrides `set_pebble_function`. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_pebble_not_void: a_pebble /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_assigned: pebble = a_pebble set_pebble_function (a_function: FUNCTION [detachable ANY]) -- Set a_function to compute `pebble`. -- It will be called once each time a pick occurs, the result -- will be assigned to `pebble` for the duration of transport. -- When a pick occurs, the pick position in widget coordinates, -- <<x, y>> in pixels, is passed. -- To handle this data use a_function of type -- FUNCTION [ANY, TUPLE [INTEGER, INTEGER], ANY] and return the -- pebble as a function of x and y. -- Overrides `set_pebble`. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_function_not_void: a_function /= Void a_function_takes_two_integer_open_operands: a_function.valid_operands ([1, 1]) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_function_assigned: pebble_function = a_function set_pebble_position (a_x, a_y: INTEGER_32) -- Set the initial position for pick and drop -- Coordinates are in pixels and are relative to position of Current. -- Pebble_positioning_enabled must be True for the position to be used, -- use enable_pebble_positioning. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y set_pick_and_drop_mode -- Set user interface mode to pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE pick_and_drop_set: mode_is_pick_and_drop set_real_source (dockable_source: EV_DOCKABLE_SOURCE) -- Assign dockable_source to `real_source`. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable dockable_source_not_void: dockable_source /= Void dockable_source_is_parent_recursive: source_has_current_recursive (dockable_source) ensure -- from EV_DOCKABLE_SOURCE real_source_assigned: real_source = dockable_source set_real_target (a_target: EV_DOCKABLE_TARGET) -- Assign a_target to `real_target`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed target_not_void: a_target /= Void ensure -- from EV_WIDGET assigned: real_target = a_target set_row_editable (a_flag: BOOLEAN; i: INTEGER_32) -- Make row at index 'i' editable according to 'a_flag'. set_target_data_function (a_function: FUNCTION [like pebble, EV_PND_TARGET_DATA]) -- Set a_function to compute target meta data based on transport source. -- Overrides any `target_name` set with `set_target_name`. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_function_not_void: a_function /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE target_data_function_assigned: target_data_function /= Void and then target_data_function.is_equal (a_function) set_target_menu_mode -- Set user interface mode to pop-up menu of targets. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure -- from EV_PICK_AND_DROPABLE target_menu_mode_set: mode_is_target_menu set_target_name (a_name: READABLE_STRING_GENERAL) -- Assign a_name to `target_name`. -- (from EV_ABSTRACT_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE a_name_not_void: a_name /= Void ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE target_name_assigned: attached target_name as l_target_name and then a_name /= l_target_name and then a_name.same_string (l_target_name) set_unique_column_values (a_flag: BOOLEAN) -- Set column value uniqueness to 'a_flag'. set_with_previous_text -- Set field at row index 'widget_row' and column index 'widget_column' with -- value of saved text after an edit has been unsuccessful show -- Request that Current be displayed when its parent is. -- True by default. -- If successful, make `is_show_requested` True. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed show_configurable_target_menu (a_x, a_y: INTEGER_32) -- Show the configurable target menu at position a_x, a_y relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed mode_is_configurable_target_menu: mode_is_configurable_target_menu configurable_menu_handler_set: configurable_target_menu_handler /= Void show_title_row -- Show row displaying column titles. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed ensure -- from EV_MULTI_COLUMN_LIST title_shown: title_shown feature -- Cursor movement back -- Move to previous position. -- (from EV_DYNAMIC_LIST) require -- from BILINEAR not_before: not before finish -- Move cursor to last position. -- (No effect if empty) -- (from CHAIN) require -- from LINEAR True ensure then -- from CHAIN at_last: not is_empty implies islast forth -- Move cursor to next position. -- (from EV_DYNAMIC_LIST) require -- from LINEAR not_after: not after ensure then -- from LIST moved_forth: index = old index + 1 go_i_th (i: INTEGER_32) -- Move cursor to i-th position. -- (from EV_DYNAMIC_LIST) require -- from CHAIN valid_cursor_index: valid_cursor_index (i) ensure -- from CHAIN position_expected: index = i go_to (p: CURSOR) -- Move cursor to position p. -- (from EV_DYNAMIC_LIST) require -- from CURSOR_STRUCTURE cursor_position_valid: valid_cursor (p) move (i: INTEGER_32) -- Move cursor i positions. -- (from EV_DYNAMIC_LIST) ensure -- from CHAIN too_far_right: (old index + i > count) implies exhausted too_far_left: (old index + i < 1) implies exhausted expected_index: (not exhausted) implies (index = old index + i) search (v: like item) -- Move to first position (at or after current -- position) where `item` and v are equal. -- If structure does not include v ensure that -- `exhausted` will be true. -- (Reference or object equality, -- based on `object_comparison`.) -- (from BILINEAR) ensure -- from LINEAR object_found: (not exhausted and object_comparison) implies v ~ item item_found: (not exhausted and not object_comparison) implies v = item start -- Move cursor to first position. -- (from EV_DYNAMIC_LIST) require -- from TRAVERSABLE True ensure then -- from CHAIN at_first: not is_empty implies isfirst ensure then -- from EV_DYNAMIC_LIST empty_implies_after: is_empty implies after feature -- Element change append (s: SEQUENCE [like item]) -- Append a copy of s. Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible sequence_not_void: s /= Void sequence_not_current: s /= Current not_parented: not s.there_exists (agent (v: like item): BOOLEAN ) ensure -- from EV_DYNAMIC_LIST count_increased: old count + s.count = count cursor_not_moved: (index = old index) or (after and old after) fill (other: CONTAINER [EV_MULTI_COLUMN_LIST_ROW]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from CHAIN) require -- from COLLECTION other_not_void: other /= Void extendible: extendible force (v: like item) -- Add v to end. Do not move cursor. -- Was declared in {EV_DYNAMIC_LIST} as synonym of `extend`. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current v_is_last: v = last count_increased: count = old count + 1 cursor_not_moved: (index = old index) or (after and old after) dl_force (v: like item) -- Add v to end. -- (from SEQUENCE) require -- from SEQUENCE extendible: extendible ensure then -- from SEQUENCE new_count: count = old count + 1 item_inserted: has (v) merge_left (other: EV_EDITABLE_LIST) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before other_exists: other /= Void not_current: other /= Current ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count new_index: index = old index + old other.count other_is_empty: other.is_empty merge_right (other: EV_EDITABLE_LIST) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after other_exists: other /= Void not_current: other /= Current ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count same_index: index = old index other_is_empty: other.is_empty put (v: like item) -- Replace current item by v. -- (Synonym for `replace`) -- (from CHAIN) require -- from CHAIN writeable: writable replaceable: replaceable ensure -- from CHAIN same_count: count = old count is_inserted: is_inserted (v) sequence_put (v: like item) -- Add v to end. -- (from SEQUENCE) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) ensure then -- from SEQUENCE new_count: count = old count + 1 put_front (v: like item) -- Add v at beginning. Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current v_is_first: v = first count_increased: count = old count + 1 cursor_not_moved: (index = old index + 1) or (before and old before) put_i_th (v: like item; i: INTEGER_32) -- Replace item at i-th position by v. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed valid_index: i > 0 and i <= count v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current item_replaced: v = i_th (i) not_has_old_item: not has (old i_th (i)) old_item_parent_void: (old i_th (i)).parent = Void count_same: count = old count cursor_not_moved: index = old index put_left (v: like item) -- Add v to the left of cursor position. Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible not_before: not before v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current v_at_index_plus_one: v = i_th (index - 1) count_increased: count = old count + 1 cursor_not_moved: index = old index + 1 put_right (v: like item) -- Add v to right of cursor position. Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible not_after: not after v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current v_at_index_plus_one: v = i_th (index + 1) count_increased: count = old count + 1 cursor_not_moved: index = old index remove_help_context -- Remove key press action associated with EV_APPLICATION.help_key. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed help_context_not_void: help_context /= Void ensure -- from EV_HELP_CONTEXTABLE no_help_context: help_context = Void remove_tooltip -- Make `tooltip` empty. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed ensure -- from EV_TOOLTIPABLE tooltip_removed: tooltip.is_empty replace (v: like item) -- Replace current item by v. -- (from EV_DYNAMIC_LIST) require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed writable: writable v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current item_replaced: v = item not_has_old_item: not has (old item) old_item_parent_void: (old item).parent = Void count_same: count = old count cursor_not_moved: index = old index resize_column_to_content (a_column: INTEGER_32) -- Resize column a_column to width of its widest text. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 0 and a_column <= column_count set_background_color (a_color: like background_color) -- Assign a_color to `background_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE background_color_assigned: background_color.is_equal (a_color) set_column_alignment (an_alignment: EV_TEXT_ALIGNMENT; a_column: INTEGER_32) -- Align the text of column a_column to an_alignment -- The first column must stay as left aligned as MSDN -- states that the first column can only be set as left aligned -- for Win32. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 1 and a_column <= column_count alignment_not_void: an_alignment /= Void ensure -- from EV_MULTI_COLUMN_LIST column_alignment_assigned: column_alignment (a_column).is_equal (an_alignment) set_column_alignments (alignments: LINKED_LIST [EV_TEXT_ALIGNMENT]) -- Assign alignments to column text alignments in order. -- The first alignment element is ignored -- (see set_column_alignment). -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed alignments_not_void: alignments /= Void ensure -- from EV_MULTI_COLUMN_LIST column_alignments_assigned: column_alignments_assigned (alignments) set_column_title (a_title: READABLE_STRING_GENERAL; a_column: INTEGER_32) -- Assign a_title to the `column_title`(a_column). -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_positive: a_column > 0 a_title_not_void: a_title /= Void ensure -- from EV_MULTI_COLUMN_LIST a_title_assigned: column_title (a_column).same_string_general (a_title) column_count_valid: column_count >= a_column cloned: column_title (a_column) /= a_title set_column_titles (titles: ARRAY [READABLE_STRING_GENERAL]) -- Assign titles to titles of columns in order. -- Current will resize if the number of titles exceeds -- `column_count`. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed titles_not_void: titles /= Void ensure -- from EV_MULTI_COLUMN_LIST column_count_valid: column_count >= titles.count column_titles_assigned: column_titles_assigned (titles) set_column_width (a_width: INTEGER_32; a_column: INTEGER_32) -- Assign a_width `column_width`(a_column). -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed a_column_within_range: a_column > 0 a_width_positive: a_width >= 0 ensure -- from EV_MULTI_COLUMN_LIST column_count_valid: column_count >= a_column a_width_assigned: a_width = column_width (a_column) set_column_widths (widths: ARRAY [INTEGER_32]) -- Assign widths to column widths in order. -- (from EV_MULTI_COLUMN_LIST) require -- from EV_MULTI_COLUMN_LIST not_destroyed: not is_destroyed widths_not_void: widths /= Void ensure -- from EV_MULTI_COLUMN_LIST column_count_valid: column_count >= widths.count column_widths_assigned: column_widths_assigned (widths) set_data (some_data: like data) -- Assign some_data to `data`. -- (from EV_ANY) require -- from EV_ANY not_destroyed: not is_destroyed ensure -- from EV_ANY data_assigned: data = some_data set_foreground_color (a_color: like foreground_color) -- Assign a_color to `foreground_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE foreground_color_assigned: foreground_color.is_equal (a_color) set_help_context (an_help_context: FUNCTION [EV_HELP_CONTEXT]) -- Assign an_help_context to `help_context`. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed an_help_context_not_void: an_help_context /= Void ensure -- from EV_HELP_CONTEXTABLE help_context_assigned: attached help_context as l_help_context and then l_help_context.is_equal (an_help_context) set_identifier_name (a_name: READABLE_STRING_GENERAL) -- Set `identifier_name` to a_name. -- (from EV_IDENTIFIABLE) require -- from EV_IDENTIFIABLE a_name_not_void: a_name /= Void a_name_not_empty: not a_name.is_empty no_period_in_name: not a_name.has ('.'.to_character_32) no_special_regexp_characters_in_name: ensure -- from EV_IDENTIFIABLE identifier_name_set: identifier_name.same_string_general (a_name) set_minimum_height (a_minimum_height: INTEGER_32) -- Set a_minimum_height in pixels to `minimum_height`. -- If `height` is less than a_minimum_height, resize. -- From now, `minimum_height` is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32) -- Assign a_minimum_height to `minimum_height` -- and a_minimum_width to `minimum_width` in pixels. -- If `width` or `height` is less than minimum size, resize. -- From now, minimum size is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user minimum_width_set_by_user_set: minimum_width_set_by_user set_minimum_width (a_minimum_width: INTEGER_32) -- Assign a_minimum_width in pixels to `minimum_width`. -- If `width` is less than a_minimum_width, resize. -- From now, `minimum_width` is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_width_set_by_user_set: minimum_width_set_by_user set_pointer_style (a_cursor: EV_POINTER_STYLE) -- Assign a_cursor to `pointer_style`. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_cursor_not_void: a_cursor /= Void ensure -- from EV_WIDGET pointer_style_assigned: attached pointer_style as l_pointer_style and then l_pointer_style.is_equal (a_cursor) set_tooltip (a_tooltip: READABLE_STRING_GENERAL) -- Assign a_tooltip to `tooltip`. -- (from EV_TOOLTIPABLE) require -- from EV_TOOLTIPABLE not_destroyed: not is_destroyed tooltip: a_tooltip /= Void ensure -- from EV_TOOLTIPABLE tooltip_assigned: tooltip.same_string_general (a_tooltip) cloned: tooltip /= a_tooltip swap (i: INTEGER_32) -- Exchange_item at i-th position with item -- at cursor position. -- (from EV_DYNAMIC_LIST) require -- from CHAIN not_off: not off valid_index: valid_index (i) ensure -- from CHAIN swapped_to_item: item = old i_th (i) swapped_from_item: i_th (i) = old item feature -- Removal dispose -- Free the entry associated with `object_id` if any -- (from IDENTIFIED) require -- from DISPOSABLE True ensure then -- from IDENTIFIED object_freed: id_freed frozen free_id -- Free the entry associated with `object_id` if any. -- (from IDENTIFIED) ensure -- from IDENTIFIED object_freed: id_freed prune (v: like item) -- Remove v if present. Do not move cursor, except if -- cursor was on v, move to right neighbor. -- (from EV_DYNAMIC_LIST) ensure then -- from EV_DYNAMIC_LIST not_has_v: not has (v) had_item_implies_parent_void: old has (v) implies (v /= Void and then v.parent = Void) had_item_implies_count_decreased: old has (v) implies count = old count - 1 had_item_and_was_after_implies_index_decreased: (old after and old has (v)) implies index = old index - 1 dl_prune (v: like item) -- Remove first occurrence of v, if any, -- after cursor position. -- If found, move cursor to right neighbor; -- if not, make structure `exhausted`. -- (from DYNAMIC_CHAIN) require -- from COLLECTION prunable: prunable prune_all (v: like item) -- Remove all occurrences of v. -- (Reference or object equality, -- based on `object_comparison`.) -- Leave structure `exhausted`. -- (from DYNAMIC_CHAIN) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION no_more_occurrences: not has (v) ensure then -- from DYNAMIC_CHAIN is_exhausted: exhausted remove -- Remove current item. Move cursor to right neighbor. -- (or `after` if no right neighbor). -- (from EV_DYNAMIC_LIST) require -- from ACTIVE prunable: prunable writable: writable ensure then -- from DYNAMIC_LIST after_when_empty: is_empty implies after ensure then -- from EV_DYNAMIC_LIST v_removed: not has (old item) parent_void: (old item).parent = Void count_decreased: count = old count - 1 index_same: index = old index remove_i_th (i: INTEGER_32) -- Remove item at index i. -- Move cursor to next neighbor (or `after` if no next neighbor) if it is at i-th position. -- Do not change cursor otherwise. -- (from DYNAMIC_CHAIN) require -- from DYNAMIC_TABLE prunable: prunable valid_key: valid_index (i) ensure then -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index_if_below: index <= i implies index = old index new_index_if_above: index > i implies index = old index - 1 same_leading_items: ∀ c: old twin ¦ @ c.target_index < i implies c = i_th (.target_index) same_trailing_items: ∀ c: old twin ¦ .target_index > i implies c = i_th (.target_index - 1) remove_left -- Remove item to left of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN left_exists: index > 1 ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 new_index: index = old index - 1 ensure then -- from EV_DYNAMIC_LIST left_neighbor_removed: not has (old i_th (index - 1)) parent_void: (old i_th (index - 1)).parent = Void index_decreased: index = old index - 1 remove_right -- Remove item to right of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN right_exists: index < count ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index: index = old index ensure then -- from EV_DYNAMIC_LIST right_neighbor_removed: not has (old i_th (index + 1)) parent_void: (old i_th (index + 1)).parent = Void index_same: index = old index remove_selected_item -- Remove the currently selected item from the list. wipe_out -- Remove all items. -- (from EV_DYNAMIC_LIST) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION wiped_out: is_empty ensure then -- from DYNAMIC_LIST is_before: before feature -- Conversion linear_representation: LINEAR [EV_MULTI_COLUMN_LIST_ROW] -- Representation as a linear structure -- (from LINEAR) require -- from CONTAINER True feature -- Duplication frozen deep_copy (other: EV_EDITABLE_LIST) -- 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_EDITABLE_LIST -- 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_EDITABLE_LIST) -- 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_EDITABLE_LIST -- 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_EDITABLE_LIST -- New object equal to Current -- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations frozen default: detachable EV_EDITABLE_LIST -- 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 refresh_now -- Force an immediate redraw of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed feature -- Inapplicable dl_append (s: SEQUENCE [EV_MULTI_COLUMN_LIST_ROW]) -- Append a copy of s. -- (from EV_DYNAMIC_LIST) require -- from SEQUENCE argument_not_void: s /= Void ensure -- from SEQUENCE new_count: count >= old count dl_extend (v: like item) -- Add a new occurrence of v. -- (from EV_DYNAMIC_LIST) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) dl_put_front (v: like item) -- Add v at beginning. -- Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 item_inserted: first = v dl_put_i_th (v: like item; i: INTEGER_32) -- Put v at i-th position. -- (from EV_DYNAMIC_LIST) require -- from TABLE valid_key: valid_index (i) require -- from TABLE valid_key: valid_index (i) ensure -- from TABLE inserted: i_th (i) = v dl_put_left (v: like item) -- Add v to the left of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 new_index: index = old index + 1 dl_put_right (v: like item) -- Add v to the right of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 same_index: index = old index dl_replace (v: like item) -- Replace current item by v. -- (from EV_DYNAMIC_LIST) require -- from ACTIVE writable: writable replaceable: replaceable ensure -- from ACTIVE item_replaced: item = v feature -- Implementation Changeable_comparison_criterion: BOOLEAN = False -- May `object_comparison` be changed? -- (Answer: no by default. -- (from EV_ITEM_LIST) feature -- Actions end_edit_actions: EV_LITE_ACTION_SEQUENCE -- List of actions to perform when list row has just been edited. feature -- Command destroy -- Destroy underlying native toolkit object. -- Render Current unusable. -- (from EV_ANY) ensure -- from EV_ANY is_destroyed: is_destroyed feature -- Contract support is_background_color_void: BOOLEAN -- If `background_color` void? -- (from EV_COLORIZABLE) is_bridge_ok (a_string: STRING_32): BOOLEAN -- If a_string equal implementation's `tooltip`? -- (from EV_TOOLTIPABLE) is_cloned (a_string: STRING_32): BOOLEAN -- If a_string same instance as implementation's `tooltip`? -- (from EV_TOOLTIPABLE) is_foreground_color_void: BOOLEAN -- If `foreground_color` void? -- (from EV_COLORIZABLE) is_in_default_state: BOOLEAN -- Is Current in its default state? -- (from EV_MULTI_COLUMN_LIST) require -- from EV_ANY True is_parent_recursive (a_row: EV_MULTI_COLUMN_LIST_ROW): BOOLEAN -- Is a_row a parent of Current? -- (from EV_MULTI_COLUMN_LIST) require -- from EV_DYNAMIC_LIST a_list_not_void: a_row /= Void not_destroyed: not is_destroyed parent_of_source_allows_docking: BOOLEAN -- Does parent of source to be transported -- allow current to be dragged out? (See `real_source`) -- Not all Vision2 containers are currently supported by this -- mechanism, only descendents of EV_DOCKABLE_TARGET -- are supported. -- (from EV_DOCKABLE_SOURCE) same (other: EV_ANY): BOOLEAN -- Is other Current? -- (from EV_DYNAMIC_LIST) source_has_current_recursive (source: EV_DOCKABLE_SOURCE): BOOLEAN -- Does source recursively contain Current? -- As seen by parenting structure. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed source_not_void: source /= Void feature -- Editing edit_row (x, y, button: INTEGER_32; x_tilt, y_tilt, pressure: REAL_64; a_screen_x, a_screen_y: INTEGER_32) -- User has double clicked list row so set up dialogs for in-place editing. feature -- Element Change extend (v: like item) -- Add 'v' to Current. require -- from EV_DYNAMIC_LIST not_destroyed: not is_destroyed extendible: extendible v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: not same (v) v_not_parent_of_current: not is_parent_recursive (v) ensure -- from EV_DYNAMIC_LIST parent_is_current: v.parent = Current v_is_last: v = last count_increased: count = old count + 1 cursor_not_moved: (index = old index) or (after and old after) feature -- Event handling column_resized_actions: EV_COLUMN_ACTION_SEQUENCE -- Actions to be performed when a column has been resized. -- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES) ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES not_void: Result /= Void column_title_click_actions: EV_COLUMN_ACTION_SEQUENCE -- Actions to be performed when a column title is clicked. -- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES) ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES not_void: Result /= Void conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void deselect_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE -- Actions to be performed when a row is deselected. -- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES) ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES not_void: Result /= Void dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed after a dock completes from Current. -- Either to a dockable target or a dockable dialog. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a dockable source is dragged. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void dpi_changed_actions: EV_DPI_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void file_drop_actions: EV_LITE_ACTION_SEQUENCE [LIST [STRING_32]] -- Actions to be performed when an OS file drop is performed on Current. -- (from EV_WIDGET_ACTION_SEQUENCES) focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is gained. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is lost. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE -- Actions to be performed when a keyboard press generates a displayable character. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_release_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE -- Actions to be performed when mouse wheel is rotated. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pick_actions: EV_PND_START_ACTION_SEQUENCE -- Actions to be performed when `pebble` is picked up. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE -- Actions to be performed when a transport from Current ends. -- If transport completed successfully, then event data -- is target. If cancelled, then event data is Void. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer is double clicked. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer enters widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer leaves widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE -- Actions to be performed when screen pointer moves. -- (from EV_WIDGET_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void resize_actions: EV_GEOMETRY_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void select_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE -- Actions to be performed when a row is selected. -- (from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES) ensure -- from EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES not_void: Result /= Void feature -- Iteration do_all (action: PROCEDURE [EV_MULTI_COLUMN_LIST_ROW]) -- Apply action to every item. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE action_exists: action /= Void do_if (action: PROCEDURE [EV_MULTI_COLUMN_LIST_ROW]; test: FUNCTION [EV_MULTI_COLUMN_LIST_ROW, BOOLEAN]) -- Apply action to every item that satisfies test. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE action_exists: action /= Void test_exists: test /= Void for_all (test: FUNCTION [EV_MULTI_COLUMN_LIST_ROW, BOOLEAN]): BOOLEAN -- Is test true for all items? -- Semantics not guaranteed if test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE test_exists: test /= Void ensure then -- from LINEAR empty: is_empty implies Result there_exists (test: FUNCTION [EV_MULTI_COLUMN_LIST_ROW, BOOLEAN]): BOOLEAN -- Is test true for at least one item? -- Semantics not guaranteed if test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE test_exists: test /= Void feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Selection select_item (a_string: READABLE_STRING_GENERAL; i: INTEGER_32) -- Select in list the first item with text 'a_string' at index 'i'. feature -- Status Report is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY) ensure -- from EV_ANY bridge_ok: Result = implementation.is_destroyed invariant has_relative_window: relative_window /= Void change_widgets_not_void: change_widgets /= Void editable_columns_not_void: editable_columns /= Void -- from EV_WIDGET is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested parent_contains_current: is_usable and then attached parent as l_parent implies l_parent.has (Current) -- from EV_PICK_AND_DROPABLE user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1 -- from EV_ANY is_initialized: is_initialized default_create_called: default_create_called is_coupled: default_create_called implies (implementation.interface = Current or (attached {EV_ENVIRONMENT} Current and then attached implementation.interface)) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from EV_POSITIONED width_not_negative: is_usable implies width >= 0 height_not_negative: is_usable implies height >= 0 minimum_width_not_negative: is_usable implies minimum_width >= 0 minimum_height_not_negative: is_usable implies minimum_height >= 0 -- from EV_DOCKABLE_SOURCE parent_permits_docking: is_dockable implies parent_of_source_allows_docking -- from EV_COLORIZABLE background_color_not_void: is_usable implies not is_background_color_void foreground_color_not_void: is_usable implies not is_foreground_color_void -- from EV_ITEM_LIST parent_of_items_is_current: is_usable and then not is_empty implies parent_of_items_is_current items_unique: is_usable and not is_empty implies items_unique -- from LIST before_definition: before = (index = 0) after_definition: after = (index = count + 1) -- from CHAIN non_negative_index: index >= 0 index_small_enough: index <= count + 1 off_definition: off = ((index = 0) or (index = count + 1)) isfirst_definition: isfirst = ((not is_empty) and (index = 1)) islast_definition: islast = ((not is_empty) and (index = count)) item_corresponds_to_index: (not off) implies (item = i_th (index)) -- from ACTIVE writable_constraint: writable implies readable empty_constraint: is_empty implies (not readable) and (not writable) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= count or else Lower = count + 1 -- from BILINEAR not_both: not (after and before) before_constraint: before implies off -- from LINEAR after_constraint: after implies off -- from TRAVERSABLE empty_constraint: is_empty implies off -- from FINITE empty_definition: is_empty = (count = 0) -- from EV_ITEM_PIXMAP_SCALER pixmaps_size_positive: pixmaps_height > 0 and pixmaps_width > 0 note copyright: "Copyright (c) 1984-2023, 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_EDITABLE_LIST -- Generated by Eiffel Studio --
For more details: eiffel.org