Automatic generation produced by ISE Eiffel
note description: "[ Grid items that do not redraw themselves. The `expose_actions` are fired as Current must be redrawn, and provide the drawable into which you must draw. The upper left corner of the item starts at coordinates 0x0 in the passed drawable. All drawing Performed in the drawable is clipped to `width`, `height` of Current. Note that the dimensions of the drawable area are undefined, but are always be greater than `width` and `height`. Note also that like a EV_DRAWING_AREA the content of the area is unspecified when the `expose_actions` are called, therefore you might have to clear its content before drawing to ensure proper behavior. ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2015-12-17 04:34:17 -0900 (Thu, 17 Dec 2015) $" revision: "$Revision: 98279 $" class interface EV_GRID_DRAWABLE_ITEM create default_create -- Standard creation procedure. -- (from EV_ANY) require -- from ANY True ensure then -- from EV_ANY is_coupled: implementation /= Void is_initialized: is_initialized default_create_called: default_create_called is_in_default_state: is_in_default_state make_with_expose_action_agent (an_agent: PROCEDURE [EV_DRAWABLE]) -- Create Current and add an_agent to `expose_actions`. require an_agent_not_void: an_agent /= Void feature -- Access attached_parent: EV_GRID -- Attached grid in which Current is contained. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM parent /= Void background_color: detachable EV_COLOR -- Color displayed behind foreground features. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed column: EV_GRID_COLUMN -- Column to which current item belongs. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed is_parented: is_parented ensure -- from EV_GRID_ITEM column_not_void: Result /= Void 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) foreground_color: detachable EV_COLOR -- Color of foreground features like text. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed full_identifier_path: STRING_32 -- Full name of object by prepending path of parent -- Uses '.' as a separator. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_correct: parent = Void implies Result.is_equal (identifier_name) result_correct: attached parent as l_parent implies Result.is_equal (l_parent.full_identifier_path + ".".as_string_32 + identifier_name) generating_type: TYPE [detachable EV_GRID_DRAWABLE_ITEM] -- 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 height: INTEGER_32 -- Height of Current in pixels. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM result_non_negative: Result >= 0 horizontal_indent: INTEGER_32 -- Horizontal distance in pixels from left edge of Current to left edge of `column`. -- This may not be set, but the value is determined by the current tree structure -- of `parent` and `row`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM not_parent_tree_enabled_implies_result_zero: attached parent and then ((attached parent as l_parent and then not l_parent.is_tree_enabled) implies Result = 0) parent_tree_enabled_implies_result_greater_or_equal_to_zero: attached parent and then ((attached parent as l_parent and then l_parent.is_tree_enabled) implies Result >= 0) 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) parent: detachable EV_GRID -- Grid in which Current is contained if any. -- (from EV_GRID_ITEM) 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 required_width: INTEGER_32 -- Width in pixels required to fully display contents, based -- on current settings. -- Note that in some descendents such as EV_GRID_DRAWABLE_ITEM, this -- returns 0. For such items, `set_required_width` is available. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM result_non_negative: Result >= 0 row: EV_GRID_ROW -- Row to which current item belongs. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM row_not_void: Result /= Void tooltip: detachable STRING_32 -- Tooltip displayed on Current. -- If Result is Void or is_empty then no tooltip is displayed. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed virtual_x_position: INTEGER_32 -- Horizontal offset of Current in relation to the -- the virtual area of `parent` grid in pixels. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM valid_result: attached parent as l_parent implies Result >= 0 and Result <= l_parent.virtual_width - column.width + horizontal_indent virtual_y_position: INTEGER_32 -- Vertical offset of Current in relation to the -- the virtual area of `parent` grid in pixels. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM valid_result_when_parent_row_height_fixed: attached parent as l_parent and then l_parent.is_row_height_fixed implies Result >= 0 and Result <= l_parent.virtual_height - l_parent.row_height valid_result_when_parent_row_height_not_fixed: attached parent as l_parent and then not l_parent.is_row_height_fixed implies Result >= 0 and Result <= l_parent.virtual_height - row.height width: INTEGER_32 -- Width of Current in pixels. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented ensure -- from EV_GRID_ITEM result_non_negative: Result >= 0 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_DRAWABLE_ITEM): 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_DRAWABLE_ITEM): 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_DRAWABLE_ITEM): 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 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 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) is_displayed: BOOLEAN -- Is Current visible on the screen? -- An item that is_displayed does not necessarily have to be visible on screen at that particular time. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM bridge_ok: Result = implementation.is_displayed is_parented: BOOLEAN -- Does current item belong to an EV_GRID? -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed is_selectable: BOOLEAN -- May `enable_select` be called? -- (from EV_SELECTABLE) require -- from EV_SELECTABLE not_destroyed: not is_destroyed is_selected: BOOLEAN -- Is selected? -- (from EV_SELECTABLE) require -- from EV_SELECTABLE not_destroyed: not is_destroyed ensure -- from EV_SELECTABLE bridge_ok: is_selectable implies Result = implementation.is_selected is_tab_navigatable: BOOLEAN -- Is Current tab key navigatable? -- Used to determine whether it may be tabbed to if is_item_tab_navigation_enabled is True. -- Set via `set_is_tab_navigatable`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed 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)) feature -- Status setting disable_select -- Deselect the object. -- (from EV_DESELECTABLE) require -- from EV_DESELECTABLE not_destroyed: not is_destroyed ensure -- from EV_DESELECTABLE unselected: action_sequence_call_counter = old action_sequence_call_counter implies not is_selected enable_select -- Make `is_selected` True. -- (from EV_SELECTABLE) require -- from EV_SELECTABLE not_destroyed: not is_destroyed is_selectable: is_selectable ensure -- from EV_SELECTABLE is_selected: action_sequence_call_counter = old action_sequence_call_counter implies is_selected ensure_visible -- Ensure Current is visible in viewable area of `parent`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: parent /= Void is_displayed: is_displayed ensure -- from EV_GRID_ITEM virtual_x_position_not_changed_if_indent_greater_or_equal_to_column_width: old (horizontal_indent > column.width) implies old virtual_x_position = virtual_x_position virtual_x_position_not_changed_if_item_already_visible: old (virtual_x_position >= attached_parent.virtual_x_position) and old (virtual_x_position + width <= attached_parent.virtual_x_position + attached_parent.viewable_width) implies old (virtual_x_position = virtual_x_position) virtual_y_position_not_changed_if_item_already_visible: old (virtual_y_position >= attached_parent.virtual_y_position) and old (virtual_y_position + height <= attached_parent.virtual_y_position + attached_parent.viewable_height) implies old (virtual_y_position = virtual_y_position) row_visible_when_heights_fixed_in_parent: attached_parent.is_row_height_fixed implies row.virtual_y_position >= attached_parent.virtual_y_position and virtual_y_position + attached_parent.row_height <= attached_parent.virtual_y_position + (attached_parent.viewable_height).max (attached_parent.row_height) row_visible_when_heights_not_fixed_in_parent: not attached_parent.is_row_height_fixed implies row.virtual_y_position >= attached_parent.virtual_y_position and virtual_y_position + row.height <= attached_parent.virtual_y_position + (attached_parent.viewable_height).max (row.height) virtual_x_position_visible_if_indent_less_than_column_width: horizontal_indent < column.width implies virtual_x_position >= attached_parent.virtual_x_position and virtual_x_position + width <= attached_parent.virtual_x_position + (attached_parent.viewable_width).max (width) set_background_color (a_color: like background_color) -- Assign a_color to `background_color`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM background_color_assigned: background_color = a_color set_foreground_color (a_color: like foreground_color) -- Assign a_color to `foreground_color`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM foreground_color_assigned: foreground_color = a_color set_is_tab_navigatable (a_is_tab_navigatable: BOOLEAN) -- Set tab navigatable state to a_is_tab_navigatable -- Used to determine whether it may be tabbed to if a_is_tab_navigatable is True. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM is_tab_navigatable_set: is_tab_navigatable = a_is_tab_navigatable set_required_width (a_required_width: INTEGER_32) -- Assign a_required_width to `required_width`. require not_destroyed: not is_destroyed a_required_width_non_negative: a_required_width >= 0 ensure required_width_set: required_width = a_required_width set_tooltip (a_tooltip: detachable READABLE_STRING_GENERAL) -- Assign a_tooltip to `tooltip`. -- pass Void to remove the tooltip. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed ensure -- from EV_GRID_ITEM tooltip_reset: a_tooltip = Void implies tooltip = Void tooltip_set: a_tooltip /= Void implies (attached tooltip as l_tooltip and then a_tooltip.as_string_32 ~ l_tooltip) toggle -- Change `is_selected`. -- (from EV_DESELECTABLE) require -- from EV_DESELECTABLE not_is_destroyed: not is_destroyed can_be_selected: not is_selected implies is_selectable ensure -- from EV_DESELECTABLE is_selected_changed: action_sequence_call_counter = old action_sequence_call_counter implies is_selected /= old is_selected feature -- Element change expose_actions: EV_LITE_ACTION_SEQUENCE [EV_DRAWABLE] -- Actions to be performed when an area needs to be redrawn. -- See description at top of class to determine how to draw into the drawable. ensure not_void: Result /= Void 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_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) feature -- Duplication frozen deep_copy (other: EV_GRID_DRAWABLE_ITEM) -- 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_DRAWABLE_ITEM -- 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_DRAWABLE_ITEM) -- 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_DRAWABLE_ITEM -- 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_DRAWABLE_ITEM -- New object equal to Current -- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations frozen default: detachable EV_GRID_DRAWABLE_ITEM -- 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 feature -- Actions activate -- Setup Current for interactive in-place editing of Current. -- Activation is usually achieved by connecting an agent to -- {EV_GRID}.pointer_double_press_actions' that calls `activate`. -- Will call `activate_action` of Current to setup the in-place editing. -- The default behavior of the activation can be overriden in {EV_GRID}.item_activate_actions, -- this is useful for repositioning the popup window used editing Current. -- The parent EV_GRID will first receive the focus before the item is activated if another widget has focus. -- See {EV_GRID_EDITABLE_ITEM}.activate_action for an example of what happens on activation. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented deactivate -- Cleanup from previous call to `activate`. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented redraw -- Force Current to be re-drawn when next idle. -- (from EV_GRID_ITEM) require -- from EV_GRID_ITEM not_destroyed: not is_destroyed parented: is_parented feature -- Command destroy -- Destroy underlying native toolkit object. -- Render Current unusable. -- (from EV_ANY) ensure -- from EV_ANY is_destroyed: is_destroyed feature -- Event handling activate_actions: EV_LITE_ACTION_SEQUENCE [EV_POPUP_WINDOW] -- Actions to be performed to override the default `activate` setup of Current, see {EV_GRID_EDITABLE_ITEM}.activate_action. -- Useful for repositioning popup_window, which will then be shown automatically by the grid. -- Arguments of TUPLE (with name for clarity): -- -- popup_window: EV_POPUP_WINDOW -- The popup window used to interactively edit activate_item, window has already been sized and positioned. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES result_not_void: Result /= Void deactivate_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when Current has been deactivated. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES result_not_void: Result /= Void deselect_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when Current is deselected. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES result_not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_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_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES not_void: Result /= Void pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer enters widget. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES not_void: Result /= Void pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer leaves widget. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES not_void: Result /= Void pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE -- Actions to be performed when screen pointer moves. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES not_void: Result /= Void select_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when Current is selected. -- (from EV_GRID_ITEM_ACTION_SEQUENCES) ensure -- from EV_GRID_ITEM_ACTION_SEQUENCES result_not_void: Result /= Void feature -- Markers fixme (comment: READABLE_STRING_8) -- Mark code that has to be "fixed" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class to_implement (comment: READABLE_STRING_8) -- Mark code that has to be "implemented" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class to_implement_assertion (comment: READABLE_STRING_8): BOOLEAN -- Mark assertion that has to be "implemented" with comment. -- (from REFACTORING_HELPER) require -- from REFACTORING_HELPER comment_not_void: comment /= Void ensure -- from REFACTORING_HELPER instance_free: class feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Status Report is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY) ensure -- from EV_ANY bridge_ok: Result = implementation.is_destroyed invariant -- from EV_GRID_ITEM parented_implies_height_equals_row_height_or_parent_row_height: (attached parent as l_parent and then not l_parent.is_row_height_fixed implies height = row.height) or (attached parent as l_parent and then l_parent.is_row_height_fixed implies height = l_parent.row_height) parented_and_parent_has_no_tree_implies_width_equals_column_width: attached parent as l_parent and then not l_parent.is_tree_enabled implies width = column.width parented_and_row_is_subrow_implies_width_equals_column_width_less_indent: attached parent as l_parent and row.parent_row /= Void implies width = (column.width - horizontal_indent).max (0) -- 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_DESELECTABLE not_selectable_therefore_not_selected: not is_selectable implies not is_selected note copyright: "Copyright (c) 1984-2006, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 356 Storke Road, Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class EV_GRID_DRAWABLE_ITEM -- Generated by Eiffel Studio --
For more details: eiffel.org