Automatic generation produced by ISE Eiffel

Classes Clusters Cluster hierarchy Chart Relations Flat contracts Go to:
note description: "[ An EV_FIGURE_WORLD_CELL is an EV_CELL with scrollbars displaying world in the cell. Whenever the world does not fit into the frame the scrolling area is resized to make sure that every part of the world is reachable through the scrollbars. If a figure is moved closer to the frame border then autoscroll_border the frame starts to scroll. If the user clicks into the frame but not onto a figure the frame can be moved arround with the "hand". A buffer is used to prefend flickering. The buffer size as well as the drawing_area size is constant no matter how large the world is. example: create figure_world_cell.make_with_world (create EV_FIGURE_WORLD) figure_world_cell.world.extend (create {EV_FIGURE_LINE}.make_with_positions (0, 0, 100, 100)) horizontal_box.extend (figure_world_cell) ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2019-03-21 02:31:08 -0800 (Thu, 21 Mar 2019) $" revision: "$Revision: 102994 $" class interface EV_MODEL_WORLD_CELL create make_with_world (a_world: like world) -- Create an EV_FIGURE_WORLD_FRAM displaying a_world. require a_world_not_void: a_world /= Void ensure world_set: world = a_world 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 autoscroll_border: INTEGER_32 -- Distance to the frame border where scrolling starts. 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) background_pixmap: detachable EV_PIXMAP -- Result is pixmap displayed on background of Current. -- It is tessellated and fills whole of Current. -- (from EV_CONTAINER) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed ensure -- from EV_PIXMAPABLE bridge_ok: (Result = Void and implementation.background_pixmap = Void) or (attached Result and then attached implementation.background_pixmap as l_pixmap and then Result.is_equal (l_pixmap)) configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY] -- Agent used for customizing the Pick and Drop Target Menu of Current. -- (from EV_PICK_AND_DROPABLE) data: detachable ANY -- Arbitrary user data may be stored here. -- (from EV_ANY) default_identifier_name: STRING_32 -- Default name if no other name is set. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_key_processing_handler: detachable PREDICATE [EV_KEY] assign set_default_key_processing_handler -- Agent used to determine whether the default key processing should occur for Current. -- If agent returns True then default key processing continues as normal, False prevents -- default key processing from occurring. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.default_key_processing_handler deny_cursor: EV_POINTER_STYLE -- Result is cursor displayed when the screen pointer is over a -- target that does not accept pebble during pick and drop. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE result_not_void: Result /= Void ensure then -- from EV_PICK_AND_DROPABLE cursor_valid: (attached implementation.deny_cursor implies Result = implementation.deny_cursor) or else Result = Default_pixmaps.No_cursor drawing_area: EV_DRAWING_AREA -- Graphical surface displaying world. ev_application: EV_APPLICATION -- Current application if created yet. -- (from EV_SHARED_APPLICATION) require -- from EV_SHARED_APPLICATION application_exists: attached Shared_environment.application same_processor_as_application: Shared_environment.is_application_processor ev_separate_application: separate EV_APPLICATION -- Current application if created yet. -- (from EV_SHARED_APPLICATION) require -- from EV_SHARED_APPLICATION application_exists: attached Shared_environment.application 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 + "." + identifier_name) generating_type: TYPE [detachable EV_MODEL_WORLD_CELL] -- 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: EV_WIDGET): BOOLEAN -- Does Current include v? -- (from EV_CELL) ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty has_recursive (an_item: like item): BOOLEAN -- Does structure include an_item or -- does any structure recursively included by structure, -- include an_item. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed help_context: detachable FUNCTION [EV_HELP_CONTEXT] -- Agent that evaluates to help context sent to help engine when help is requested -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed ensure -- from EV_HELP_CONTEXTABLE bridge_ok: Result = implementation.help_context horizontal_scrollbar: EV_HORIZONTAL_SCROLL_BAR -- Horizontal scroll bar. frozen id_object (an_id: INTEGER_32): detachable IDENTIFIED -- Object associated with an_id (void if no such object) -- (from IDENTIFIED) ensure -- from IDENTIFIED consistent: Result = Void or else Result.object_id = an_id identifier_name: STRING_32 -- Name of object -- If no specific name is set, default_identifier_name is used. -- (from EV_IDENTIFIABLE) ensure -- from EV_IDENTIFIABLE result_not_void: Result /= Void result_not_empty: not Result.is_empty no_period_in_result: not Result.has ('.'.to_character_32) default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name) is_docking_enabled: BOOLEAN -- May Current be docked to? -- If True, Current will accept docking -- from a compatible EV_DOCKABLE_SOURCE. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET bridge_ok: Result = implementation.is_docking_enabled item: EV_WIDGET -- Current item. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed readable: readable ensure -- from EV_CONTAINER bridge_ok: Result = implementation.interface_item frozen object_id: INTEGER_32 -- Unique for current object in any given session -- (from IDENTIFIED) ensure -- from IDENTIFIED valid_id: Result > 0 implies id_object (Result) = Current parent: detachable EV_CONTAINER -- Contains Current. -- (from EV_WIDGET) require -- from EV_IDENTIFIABLE not_destroyed: not is_destroyed ensure -- from EV_IDENTIFIABLE correct: has_parent implies Result /= Void correct: not has_parent implies Result = Void ensure then -- from EV_WIDGET bridge_ok: Result = implementation.parent pebble: detachable ANY -- Data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble pebble_function: detachable FUNCTION [detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_function pebble_positioning_enabled: BOOLEAN -- If True then pick and drop start coordinates are -- pebble_x_position, pebble_y_position. -- If False then pick and drop start coordinates are -- the pointer coordinates. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_positioning_enabled pebble_x_position: INTEGER_32 -- Initial x position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_x_position pebble_y_position: INTEGER_32 -- Initial y position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.pebble_y_position pointer_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 projector: EV_MODEL_WIDGET_PROJECTOR -- Projector to render world. 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 scroll_speed: REAL_64 -- Speed of auto scroll. Autoscroll happens every 200 milliseconds for -- scroll_speed * (distance between autoscroll_border and cursor) -- Pixels. Meaning the nearer the cursor is to the cell border the -- faster the scroll plus the higher the scroll_speed value the faster -- the scroll. Default is 1.0. Shared_environment: EV_ENVIRONMENT -- Shared EV_ENVIRONMENT object. -- (from EV_SHARED_APPLICATION) 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 vertical_scrollbar: EV_VERTICAL_SCROLL_BAR -- Vertical scroll bar. veto_dock_function: detachable FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN] -- Function to determine whether current dock is allowed. -- If Result is True, dock will be disallowed. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET bridge_ok: Result = implementation.veto_dock_function world: EV_MODEL_WORLD -- The world shown in Current. world_border: INTEGER_32 -- Minimal distance between world borders and frame borders. feature -- Measurement client_height: INTEGER_32 -- Height of the area available to children in pixels. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER bridge_ok: Result = implementation.client_height client_width: INTEGER_32 -- Width of the area available to children in pixels. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER bridge_ok: Result = implementation.client_width dpi: NATURAL_32 -- Window dpi -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED positive_or_zero: Result >= 0 height: INTEGER_32 -- Vertical size in pixels. -- Same as minimum_height when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.height minimum_height: INTEGER_32 -- Lower bound on height in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_height positive_or_zero: Result >= 0 minimum_width: INTEGER_32 -- Lower bound on width in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.minimum_width positive_or_zero: Result >= 0 screen_x: INTEGER_32 -- Horizontal offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_x screen_y: INTEGER_32 -- Vertical offset relative to screen. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.screen_y width: INTEGER_32 -- Horizontal size in pixels. -- Same as minimum_width when not displayed. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.width x_position: INTEGER_32 -- Horizontal offset relative to parent x_position in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.x_position y_position: INTEGER_32 -- Vertical offset relative to parent y_position in pixels. -- (from EV_POSITIONED) require -- from EV_POSITIONED not_destroyed: not is_destroyed ensure -- from EV_POSITIONED bridge_ok: Result = implementation.y_position feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal (other: EV_MODEL_WORLD_CELL): 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_MODEL_WORLD_CELL): 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 (other: EV_MODEL_WORLD_CELL): 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 count: INTEGER_32 -- Number of items in Current. -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure then -- from EV_CELL valid_result: Result = 0 or Result = 1 extendible: BOOLEAN -- Is there no element? -- Was declared in EV_CELL as synonym of is_empty. -- (from EV_CELL) full: BOOLEAN -- Is structure filled to capacity? -- (from EV_CELL) has_capture: BOOLEAN -- Does widget have capture? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_capture has_focus: BOOLEAN -- Does widget have the keyboard focus? -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET bridge_ok: Result = implementation.has_focus has_identifier_name_set: BOOLEAN -- Is a specific identifier name set? -- (from EV_IDENTIFIABLE) has_parent: BOOLEAN -- Does identifiable has a parent? -- (from EV_IDENTIFIABLE) frozen id_freed: BOOLEAN -- Has Current been removed from the table? -- (from IDENTIFIED) is_autoscroll_enabled: BOOLEAN -- Is autoscroll enabled? 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 there no element? -- Was declared in EV_CELL as synonym of extendible. -- (from EV_CELL) is_external_docking_enabled: BOOLEAN -- Is Current able to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport? -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_enabled is_external_docking_relative: BOOLEAN -- Will dockable dialog displayed when Current is docked externally -- be displayed relative to parent window of Current? -- Otherwise displayed as a standard window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.is_external_docking_relative is_inserted (v: EV_WIDGET): BOOLEAN -- Has v been inserted by the most recent insertion? -- (By default, the value returned is equivalent to calling -- has (v). However, descendants might be able to provide more -- efficient implementations.) -- (from COLLECTION) is_resize_enabled: BOOLEAN -- Is resizing enabled? is_scrollbar_enabled: BOOLEAN -- Are scrollbars visible? 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 merged_radio_button_groups: detachable ARRAYED_LIST [EV_CONTAINER] -- Result is all other radio button groups -- merged with Current. Void if no other containers -- are merged. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER not_is_empty: Result /= Void implies not Result.is_empty mode_is_configurable_target_menu: BOOLEAN -- Is the user interface mode a configurable pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_configurable_target_menu mode_is_drag_and_drop: BOOLEAN -- Is the user interface mode drag and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_drag_and_drop mode_is_pick_and_drop: BOOLEAN -- Is the user interface mode pick and drop? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_pick_and_drop mode_is_target_menu: BOOLEAN -- Is the user interface mode a pop-up menu of targets? -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed ensure then -- from EV_PICK_AND_DROPABLE bridge_ok: Result = implementation.mode_is_target_menu object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? -- (from EV_CELL) readable: BOOLEAN -- Is there a current item that may be accessed? -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed real_source: detachable EV_DOCKABLE_SOURCE -- Result is source to be dragged --  when a docking drag occurs on Current. -- If Void, Current is dragged. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE bridge_ok: Result = implementation.real_source same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) writable: BOOLEAN -- Is there a current item that may be modified? -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed feature -- Status setting center_pointer -- Position screen pointer over center of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: Changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison disable_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_docking -- Ensure is_docking_enabled is False. -- Current will not accept docking. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET not_dockable: not is_docking_enabled disable_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_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_resize -- Set is_resize_enabled to False. ensure set: is_resize_enabled = False disable_scrollbars -- Hide scrollbars. ensure hide: not horizontal_scrollbar.is_show_requested and not vertical_scrollbar.is_show_requested set: not is_scrollbar_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 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_docking -- Ensure is_docking_enabled is True. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_TARGET is_dockable: is_docking_enabled enable_external_docking -- Assign True to is_external_docking_enabled. -- Allows Current to be docked into an EV_DOCKABLE_DIALOG -- When there is no valid EV_DRAGABLE_TARGET upon completion -- of transport. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed is_dockable: is_dockable ensure -- from EV_DOCKABLE_SOURCE is_externally_dockable: is_external_docking_enabled enable_external_docking_relative -- Assign True to is_external_docking_relative, ensuring that -- a dockable dialog displayed when Current is docked externally -- is displayed relative to the top level window. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed external_docking_enabled: is_external_docking_enabled ensure -- from EV_DOCKABLE_SOURCE external_docking_not_relative: is_external_docking_relative enable_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_resize -- Set is_resize_enabled to True. ensure set: is_resize_enabled = True enable_scrollbars -- Show scrollbars. ensure show: horizontal_scrollbar.is_show_requested and vertical_scrollbar.is_show_requested set: is_scrollbar_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 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 merge_radio_button_groups (other: EV_CONTAINER) -- Merge Current radio button group with that of other. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed other_not_void: other /= Void 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 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_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_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_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_veto_dock_function (a_function: FUNCTION [EV_DOCKABLE_SOURCE, BOOLEAN]) -- Assign a_function to veto_dock_function. -- (from EV_DOCKABLE_TARGET) require -- from EV_DOCKABLE_TARGET not_destroyed: not is_destroyed a_function_not_void: a_function /= Void ensure -- from EV_DOCKABLE_TARGET veto_function_set: veto_dock_function = a_function 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 unmerge_radio_button_groups (other: EV_CONTAINER) -- Remove other from radio button group of Current. -- If no radio button of other was checked before removal -- then first radio button contained will be checked. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed other_is_merged: attached merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_groups.has (other) ensure -- from EV_CONTAINER other_not_merged: other.merged_radio_button_groups = Void not_contained_in_this_group: attached merged_radio_button_groups as l_merged_r_b_groups implies not l_merged_r_b_groups.has (other) other_first_radio_button_now_selected: not old other.has_selected_radio_button and old other.has_radio_button implies other.first_radio_button_selected original_radio_button_still_selected: old has_selected_radio_button implies has_selected_radio_button other_first_radio_button_now_selected: not old has_selected_radio_button and old other.has_radio_button and (attached old merged_radio_button_groups as l_merged_r_b_groups and then l_merged_r_b_groups.count = 1) and has_radio_button implies first_radio_button_selected other_original_radio_button_still_selected: old other.has_selected_radio_button implies other.has_selected_radio_button feature -- Element change crop -- Resize Scrollbars such that world plus world_border plus autoscroll_border fits in cell. extend (v: like item) -- Ensure that structure includes v. -- Do not move cursor. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed extendible: extendible v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: v /= Current v_not_parent_of_current: not is_parent_recursive (v) v_containable: may_contain (v) ensure -- from EV_CONTAINER has_v: has (v) fill (other: CONTAINER [EV_WIDGET]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from COLLECTION) require -- from COLLECTION other_not_void: other /= Void extendible: extendible fit_to_screen -- Zoom world such that it fits to screen. put (v: like item) -- Replace item with v. -- Was declared in EV_CONTAINER as synonym of replace. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: writable v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: v /= Current v_not_parent_of_current: not is_parent_recursive (v) v_containable: may_contain (v) ensure -- from EV_CONTAINER has_v: has (v) not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has (l_item)) remove_help_context -- Remove key press action associated with EV_APPLICATION.help_key. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed help_context_not_void: help_context /= Void ensure -- from EV_HELP_CONTEXTABLE no_help_context: help_context = Void remove_background_pixmap -- Remove image displayed on Current. -- (from EV_PIXMAPABLE) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed ensure -- from EV_PIXMAPABLE pixmap_removed: background_pixmap = Void replace (v: like item) -- Replace item with v. -- Was declared in EV_CONTAINER as synonym of put. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: writable v_not_void: v /= Void v_parent_void: v.parent = Void v_not_current: v /= Current v_not_parent_of_current: not is_parent_recursive (v) v_containable: may_contain (v) ensure -- from EV_CONTAINER has_v: has (v) not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has (l_item)) resize_if_necessary -- Resize the scroll bars to fit in world. set_autoscroll_border (a_border: like autoscroll_border) -- Set autoscroll_border to a_border. require a_border_positive: a_border >= 0 ensure set: autoscroll_border = a_border set_background_color (a_color: like background_color) -- Assign a_color to background_color. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE background_color_assigned: background_color.is_equal (a_color) set_data (some_data: like data) -- Assign some_data to data. -- (from EV_ANY) require -- from EV_ANY not_destroyed: not is_destroyed ensure -- from EV_ANY data_assigned: data = some_data set_foreground_color (a_color: like foreground_color) -- Assign a_color to foreground_color. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE foreground_color_assigned: foreground_color.is_equal (a_color) set_help_context (an_help_context: FUNCTION [EV_HELP_CONTEXT]) -- Assign an_help_context to help_context. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed an_help_context_not_void: an_help_context /= Void ensure -- from EV_HELP_CONTEXTABLE help_context_assigned: attached help_context as l_help_context and then l_help_context.is_equal (an_help_context) set_identifier_name (a_name: READABLE_STRING_GENERAL) -- Set identifier_name to a_name. -- (from EV_IDENTIFIABLE) require -- from EV_IDENTIFIABLE a_name_not_void: a_name /= Void a_name_not_empty: not a_name.is_empty no_period_in_name: not a_name.has ('.'.to_character_32) no_special_regexp_characters_in_name: ensure -- from EV_IDENTIFIABLE identifier_name_set: identifier_name.same_string_general (a_name) set_minimum_height (a_minimum_height: INTEGER_32) -- Set a_minimum_height in pixels to minimum_height. -- If height is less than a_minimum_height, resize. -- From now, minimum_height is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32) -- Assign a_minimum_height to minimum_height -- and a_minimum_width to minimum_width in pixels. -- If width or height is less than minimum size, resize. -- From now, minimum size is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 a_minimum_height_positive: a_minimum_height >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_height_assigned: (a_minimum_height > 0 implies minimum_height = a_minimum_height) or (a_minimum_height = 0 implies (minimum_height <= 1)) minimum_height_set_by_user_set: minimum_height_set_by_user minimum_width_set_by_user_set: minimum_width_set_by_user set_minimum_width (a_minimum_width: INTEGER_32) -- Assign a_minimum_width in pixels to minimum_width. -- If width is less than a_minimum_width, resize. -- From now, minimum_width is fixed and will not be changed -- dynamically by the application anymore. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_minimum_width_positive: a_minimum_width >= 0 ensure -- from EV_WIDGET minimum_width_assigned: (a_minimum_width > 0 implies minimum_width = a_minimum_width) or (a_minimum_width = 0 implies (minimum_width <= 1)) minimum_width_set_by_user_set: minimum_width_set_by_user set_background_pixmap (a_pixmap: EV_PIXMAP) -- Display image of a_pixmap on Current. -- Image of pixmap will be a copy of a_pixmap. -- Image may be scaled in some descendents, i.e EV_TREE_ITEM -- See EV_TREE.set_pixmaps_size. -- (from EV_PIXMAPABLE) require -- from EV_PIXMAPABLE not_destroyed: not is_destroyed pixmap_not_void: a_pixmap /= Void set_pointer_style (a_cursor: EV_POINTER_STYLE) -- Assign a_cursor to pointer_style. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed a_cursor_not_void: a_cursor /= Void ensure -- from EV_WIDGET pointer_style_assigned: attached pointer_style as l_pointer_style and then l_pointer_style.is_equal (a_cursor) set_scroll_speed (a_scroll_speed: like scroll_speed) -- Set scroll_speed to a_scroll_speed. require a_scroll_speed_positive: a_scroll_speed >= 0.0 ensure set: scroll_speed = a_scroll_speed set_world (a_world: like world) -- Set world to a_world. require a_world_not_void: a_world /= Void ensure set: world = a_world set_world_border (a_border: like world_border) -- Set world_border to a_border. require a_border_positive: a_border >= 0 ensure set: world_border = a_border 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: EV_WIDGET) -- Remove v if contained. -- (from EV_CELL) require -- from EV_CONTAINER not_destroyed: not is_destroyed writable: prunable v_not_void: v /= Void v_parent_void: v.parent = Current v_not_current: v /= Current ensure -- from EV_CONTAINER has_v: not has (v) ensure then -- from EV_CELL not has (v) prune_all (v: EV_WIDGET) -- Remove all occurrences of v. -- (Reference or object equality, -- based on object_comparison.) -- (from COLLECTION) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION no_more_occurrences: not has (v) wipe_out -- Remove item. -- (from EV_CELL) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION wiped_out: is_empty feature -- Conversion linear_representation: LINEAR [like item] -- Representation as a linear structure -- (from EV_CELL) feature -- Duplication copy (other: EV_MODEL_WORLD_CELL) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from EV_ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other frozen deep_copy (other: EV_MODEL_WORLD_CELL) -- 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_MODEL_WORLD_CELL -- 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_MODEL_WORLD_CELL) -- 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_MODEL_WORLD_CELL -- 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_MODEL_WORLD_CELL -- 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_MODEL_WORLD_CELL -- 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 eif_id_object (an_id: INTEGER_32): detachable ANY -- Object associated with an_id -- (from IDENTIFIED_ROUTINES) require -- from IDENTIFIED_ROUTINES an_id_non_negative: an_id >= 0 ensure -- from IDENTIFIED_ROUTINES instance_free: class eif_object_id (an_object: ANY): INTEGER_32 -- New identifier for an_object -- (from IDENTIFIED_ROUTINES) ensure -- from IDENTIFIED_ROUTINES instance_free: class eif_object_id_positive: Result > 0 inserted: eif_id_object (Result) = an_object eif_object_id_free (an_id: INTEGER_32) -- Free the entry an_id -- (from IDENTIFIED_ROUTINES) require -- from IDENTIFIED_ROUTINES an_id_non_negative: an_id >= 0 ensure -- from IDENTIFIED_ROUTINES instance_free: class removed: eif_id_object (an_id) = Void propagate_background_color -- Propagate background_color recursively, to all children. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER background_color_propagated: background_color_propagated propagate_foreground_color -- Propagate foreground_color recursively, to all children. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed ensure -- from EV_CONTAINER foreground_color_propagated: foreground_color_propagated refresh_now -- Force an immediate redraw of Current. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed feature -- Implementation Changeable_comparison_criterion: BOOLEAN = False -- May object_comparison be changed? -- (Answer: no by default.) -- (from EV_CONTAINER) cl_extend (v: like item) -- Ensure that structure includes v. -- (from EV_CONTAINER) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) cl_prune (v: like item) -- Remove one occurrence of v if any. -- (Reference or object equality, -- based on object_comparison.) -- (from EV_CONTAINER) require -- from COLLECTION prunable: prunable cl_put (v: like item) -- Replace item with v. -- (from EV_CONTAINER) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) 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_foreground_color_void: BOOLEAN -- If foreground_color void? -- (from EV_COLORIZABLE) is_in_default_state: BOOLEAN -- Is Current in its default state? -- (from EV_CONTAINER) require -- from EV_ANY True is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN -- Is a_widget parent, or recursivly, parent of parent. -- (from EV_CONTAINER) require -- from EV_CONTAINER not_destroyed: not is_destroyed may_contain (v: EV_WIDGET): BOOLEAN -- May v be inserted in Current. -- Instances of EV_WINDOW may not be inserted -- in a container even though they are widgets. -- (from EV_CONTAINER) parent_of_source_allows_docking: BOOLEAN -- Does parent of source to be transported -- allow current to be dragged out? (See real_source) -- Not all Vision2 containers are currently supported by this -- mechanism, only descendents of EV_DOCKABLE_TARGET -- are supported. -- (from EV_DOCKABLE_SOURCE) source_has_current_recursive (source: EV_DOCKABLE_SOURCE): BOOLEAN -- Does source recursively contain Current? -- As seen by parenting structure. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed source_not_void: source /= Void feature -- Event handling conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed after a dock completes from Current. -- Either to a dockable target or a dockable dialog. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a dockable source is dragged. -- (from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_SOURCE_ACTION_SEQUENCES not_void: Result /= Void docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE -- Actions to be performed when a dockable source completes a transport -- Fired only if source has been moved, after parenting. -- (from EV_DOCKABLE_TARGET_ACTION_SEQUENCES) ensure -- from EV_DOCKABLE_TARGET_ACTION_SEQUENCES not_void: Result /= Void dpi_changed_actions: EV_DPI_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void file_drop_actions: EV_LITE_ACTION_SEQUENCE [LIST [STRING_32]] -- Actions to be performed when an OS file drop is performed on Current. -- (from EV_WIDGET_ACTION_SEQUENCES) focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is gained. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when keyboard focus is lost. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE -- Actions to be performed when a keyboard press generates a displayable character. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void key_release_actions: EV_KEY_ACTION_SEQUENCE -- Actions to be performed when a keyboard key is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE -- Actions to be performed when mouse wheel is rotated. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pick_actions: EV_PND_START_ACTION_SEQUENCE -- Actions to be performed when pebble is picked up. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE -- Actions to be performed when a transport from Current ends. -- If transport completed successfully, then event data -- is target. If cancelled, then event data is Void. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is pressed. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is released. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer is double clicked. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer enters widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when screen pointer leaves widget. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE -- Actions to be performed when screen pointer moves. -- (from EV_WIDGET_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void resize_actions: EV_GEOMETRY_ACTION_SEQUENCE -- Actions to be performed when size changes. -- (from EV_WIDGET_ACTION_SEQUENCES) ensure -- from EV_WIDGET_ACTION_SEQUENCES not_void: Result /= Void feature -- Iteration new_cursor: ITERATION_CURSOR [EV_WIDGET] -- Fresh cursor associated with current structure -- (from EV_CONTAINER) ensure -- from ITERABLE result_attached: Result /= Void feature -- 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 scroll_speed_positive: scroll_speed >= 0.0 -- from EV_CONTAINER client_width_non_negative: is_usable implies client_width >= 0 client_width_within_limit: is_usable implies client_width <= width client_height_non_negative: is_usable implies client_height >= 0 client_height_within_limit: is_usable implies client_height <= height all_radio_buttons_connected: is_usable implies all_radio_buttons_connected parent_of_items_is_current: is_usable implies parent_of_items_is_current items_unique: is_usable implies items_unique -- from EV_WIDGET is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested parent_contains_current: is_usable and then attached parent as l_parent implies l_parent.has (Current) -- from EV_PICK_AND_DROPABLE user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1 -- from EV_ANY is_initialized: is_initialized default_create_called: default_create_called is_coupled: default_create_called implies (implementation.interface = Current or (attached {EV_ENVIRONMENT} Current and then attached implementation.interface)) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from EV_POSITIONED width_not_negative: is_usable implies width >= 0 height_not_negative: is_usable implies height >= 0 minimum_width_not_negative: is_usable implies minimum_width >= 0 minimum_height_not_negative: is_usable implies minimum_height >= 0 -- from EV_DOCKABLE_SOURCE parent_permits_docking: is_dockable implies parent_of_source_allows_docking -- from EV_COLORIZABLE background_color_not_void: is_usable implies not is_background_color_void foreground_color_not_void: is_usable implies not is_foreground_color_void note copyright: "Copyright (c) 1984-2019, 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_MODEL_WORLD_CELL
Classes Clusters Cluster hierarchy Chart Relations Flat contracts Go to:

-- Generated by Eiffel Studio --
For more details: eiffel.org