Automatic generation produced by ISE Eiffel
note description: "[ A place holder zone. Normally used for place holder for editors zones. When there is no type_editor zone in docking manager, This zone is the place holder for eidtors zones, when added new editor zones to docking manager, this zone's location is the default location for editor zones. Used docking library internally. ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2017-04-14 10:05:46 -0800 (Fri, 14 Apr 2017) $" revision: "$Revision: 100203 $" class interface SD_PLACE_HOLDER_ZONE create make (a_content: SD_CONTENT; a_docking_manager: SD_DOCKING_MANAGER) -- Associate new object with a_content and a_docking_manager. require not_void: a_content /= Void only_for_place_holder_zone: a_content.unique_title.is_equal ((create {SD_SHARED} end).Editor_place_holder_content_name) ensure set: internal_content = a_content 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 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 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 SD_PLACE_HOLDER_ZONE] -- 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_cell (v: EV_WIDGET): BOOLEAN -- Does Current include v? -- (from EV_CELL) require -- from CONTAINER True 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 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 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 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 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 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 alias "≡≡≡" (other: SD_PLACE_HOLDER_ZONE): 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: SD_PLACE_HOLDER_ZONE): 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: SD_PLACE_HOLDER_ZONE): 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 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 extendible: BOOLEAN -- Is there no element? -- Was declared in {EV_CELL} as synonym of `is_empty`. -- (from EV_CELL) require -- from COLLECTION True full: BOOLEAN -- Is structure filled to capacity? -- (from EV_CELL) require -- from BOX True 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 there no element? -- Was declared in {EV_CELL} as synonym of `extendible`. -- (from EV_CELL) 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_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_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) require -- from COLLECTION True 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_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_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 extend_cell (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_cell (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 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_cell (v) not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has_cell (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_cell (v) not_has_old_item: old readable implies (attached old implementation.item as l_item and then not has_cell (l_item)) set_background_color (a_color: like background_color) -- Assign a_color to `background_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE background_color_assigned: background_color.is_equal (a_color) set_data (some_data: like data) -- Assign some_data to `data`. -- (from EV_ANY) require -- from EV_ANY not_destroyed: not is_destroyed ensure -- from EV_ANY data_assigned: data = some_data set_foreground_color (a_color: like foreground_color) -- Assign a_color to `foreground_color`. -- (from EV_COLORIZABLE) require -- from EV_COLORIZABLE not_destroyed: not is_destroyed a_color_not_void: a_color /= Void ensure -- from EV_COLORIZABLE foreground_color_assigned: foreground_color.is_equal (a_color) set_help_context (an_help_context: FUNCTION [EV_HELP_CONTEXT]) -- Assign an_help_context to `help_context`. -- (from EV_HELP_CONTEXTABLE) require -- from EV_HELP_CONTEXTABLE not_destroyed: not is_destroyed an_help_context_not_void: an_help_context /= Void ensure -- from EV_HELP_CONTEXTABLE help_context_assigned: attached help_context as l_help_context and then l_help_context.is_equal (an_help_context) set_identifier_name (a_name: READABLE_STRING_GENERAL) -- Set `identifier_name` to a_name. -- (from EV_IDENTIFIABLE) require -- from EV_IDENTIFIABLE a_name_not_void: a_name /= Void a_name_not_empty: not a_name.is_empty no_period_in_name: not a_name.has ('.'.to_character_32) no_special_regexp_characters_in_name: ensure -- from EV_IDENTIFIABLE identifier_name_set: identifier_name.same_string_general (a_name) set_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) 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_cell (v) ensure then -- from EV_CELL not has_cell (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_cell (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) require -- from CONTAINER True feature -- Duplication frozen deep_copy (other: SD_PLACE_HOLDER_ZONE) -- 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: SD_PLACE_HOLDER_ZONE -- 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: SD_PLACE_HOLDER_ZONE) -- 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: SD_PLACE_HOLDER_ZONE -- 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: SD_PLACE_HOLDER_ZONE -- 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 SD_PLACE_HOLDER_ZONE -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.`default` for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class propagate_background_color -- Propagate `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 -- Agents on_focus_in (a_content: detachable SD_CONTENT) -- Do nothing require -- from SD_ZONE has: a_content /= Void implies has (a_content) on_focus_out -- Do nothing feature -- Command add_to_container (a_container: EV_CONTAINER) -- Add Current to a_container require a_container_not_void: a_container /= Void a_container_not_full: not a_container.full clear_docking_manager -- Clear `docking_manager`. -- (from SD_DOCKING_MANAGER_HOLDER) close -- Close window. -- (from SD_DOCKING_ZONE) destroy -- Destroy underlying native toolkit object. -- Render Current unusable. -- (from EV_ANY) ensure -- from EV_ANY is_destroyed: is_destroyed disable_maximize_minimize_buttons -- Disable maximize and minimize buttons in notebook -- (from SD_UPPER_ZONE) enable_maximize_minimize_buttons -- Enable maximize and minimize buttons in notebook -- (from SD_UPPER_ZONE) expand_finish -- Do things after finish expand -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE not_void: is_expand_stack_set expand_parent_spliter (a_spliter: EV_SPLIT_AREA; a_size_to_expand: INTEGER_32) -- Try to expand a_size_to_expand -- Stop when no parent available or has already expanded a_size_to_expand -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE not_void: a_spliter /= Void extend (a_content: SD_CONTENT) -- Set a_content with Current. require -- from SD_ZONE a_content_not_void: a_content /= Void minimize -- Minimize current -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE set: is_notebook_set minimize_for_restore -- Minimize operations for restore docking layout -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE set: is_notebook_set on_minimize -- Handle minimize actions -- (from SD_UPPER_ZONE) on_normal_max_window -- Normal or max Current -- (from SD_ZONE) recover_normal_size_from_minimize -- Recover to normal zone size from minimized state -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE set: is_notebook_set ensure -- from SD_UPPER_ZONE recovered: not is_minimized recover_to_normal_state -- If Current maximized, then normal Current. -- (from SD_ZONE) set_docking_manager (a_docking_manager: like docking_manager) -- Set `docking_manager` with a_docking_manager -- (from SD_DOCKING_MANAGER_HOLDER) require -- from SD_DOCKING_MANAGER_HOLDER not_void: a_docking_manager /= Void ensure -- from SD_DOCKING_MANAGER_HOLDER set: is_docking_manager_attached set_focus_color (a_focus: BOOLEAN) -- Set title bar focuse color -- (from SD_ZONE) set_last_floating_height (a_height: INTEGER_32) -- Set last_floating_height of a zone's state -- (from SD_ZONE) require -- from SD_ZONE valid: a_height >= 0 ensure -- from SD_ZONE set: has_content implies content.state.last_floating_height = a_height set_last_floating_width (a_width: INTEGER_32) -- Set last_floating_width of zone's state -- (from SD_ZONE) require -- from SD_ZONE vaild: a_width >= 0 ensure -- from SD_ZONE set: has_content implies content.state.last_floating_width = a_width set_max (a_max: BOOLEAN) -- Set if current is maximized -- (from SD_ZONE) set_non_focus_selection_color -- Set title bar non-focuse color -- (from SD_ZONE) set_pixmap (a_pixmap: EV_PIXMAP) -- Set pixmap -- (from SD_DOCKING_ZONE) require -- from SD_DOCKING_ZONE not_void: a_pixmap /= Void set_show_normal_max (a_show: BOOLEAN) -- Do nothing set_show_stick (a_show: BOOLEAN) -- Do nothing set_title (a_title: READABLE_STRING_GENERAL) -- Do nothing require -- from SD_DOCKING_ZONE not_void: a_title /= Void update_mini_tool_bar_size -- Update mini tool bar size since client programmers mini tool bar widget size changed -- (from SD_ZONE) update_mini_toolbar -- If `content`'s mini toolbar changed, we update containers -- (from SD_DOCKING_ZONE) update_user_widget -- If `content`'s user_widget changed, we update containers -- (from SD_DOCKING_ZONE) feature -- Content issues. content: SD_CONTENT -- Content which Current holds -- (from SD_SINGLE_CONTENT_ZONE) require -- from SD_ZONE has_content: has_content valid: is_floating_zone implies child_zone_count = 1 ensure -- from SD_ZONE not_void: Result /= Void 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 -- Key feature add_hot_zones (a_docker_mediator: SD_DOCKER_MEDIATOR; a_hot_zones: ARRAYED_LIST [SD_HOT_ZONE]) -- Add hot zones -- (from SD_DOCKER_SOURCE) require -- from SD_DOCKER_SOURCE a_docker_mediator_not_void: a_docker_mediator /= Void a_hot_zones_not_void: a_hot_zones /= Void feature -- Maximum issues restore_from_maximized -- Restore to normal size if current maximized -- (from SD_ZONE) require -- from SD_UPPER_ZONE True 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 -- Query child_zone_count: INTEGER_32 -- How many zones in Current? -- (from SD_ZONE) docking_manager: SD_DOCKING_MANAGER -- Docking manager instance. -- (from SD_DOCKING_MANAGER_HOLDER) has (a_content: SD_CONTENT): BOOLEAN -- If a_content is place holder content? require -- from SD_ZONE a_content_not_void: a_content /= Void has_content: BOOLEAN -- Has content? -- (from SD_ZONE) is_docking_manager_attached: BOOLEAN -- If `docking_manager` has been set? -- (from SD_DOCKING_MANAGER_HOLDER) is_expand_stack_set: BOOLEAN -- If `expand_stack` attached? -- (from SD_UPPER_ZONE) is_floating_zone: BOOLEAN -- Is current an instance of SD_FLOATING_ZONE? -- (from SD_ZONE) is_ignore_restore_area: BOOLEAN -- If pointer in tab close button or normal/maximize button area? -- (from SD_UPPER_ZONE) is_maximized: BOOLEAN -- If current maximized? -- (from SD_ZONE) is_minimized: BOOLEAN -- If Current is minimized? -- (from SD_UPPER_ZONE) is_notebook_set: BOOLEAN -- If `internal_notebook` attached? -- (from SD_UPPER_ZONE) is_parent_split: BOOLEAN -- Is parent a split area? -- (from SD_DOCKING_ZONE) parent_split_position: INTEGER_32 -- If parent is split area, get split position -- (from SD_DOCKING_ZONE) require -- from SD_DOCKING_ZONE parent_is_split_area: is_parent_split spliter_size (a_spliter: EV_SPLIT_AREA; a_zone_size: INTEGER_32): INTEGER_32 -- Spliter size -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE not_void: a_spliter /= Void spliter_upper (a_parent: EV_CONTAINER): detachable EV_SPLIT_AREA -- Upper level spliter of a_spliter -- Void if not exists. -- (from SD_UPPER_ZONE) require -- from SD_UPPER_ZONE not_void: a_parent /= Void state: SD_STATE -- State which Current is -- (from SD_ZONE) ensure -- from SD_ZONE not_void: Result /= Void title: STRING_32 -- Title. title_area: EV_RECTANGLE -- Place holder content has zero sized title area. ensure -- from SD_DOCKING_ZONE not_void: Result /= Void type: INTEGER_32 -- Type -- (from SD_ZONE) feature -- Status Report is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY) ensure -- from EV_ANY bridge_ok: Result = implementation.is_destroyed invariant -- from EV_CONTAINER client_width_non_negative: is_usable implies 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 -- from SD_ZONE is_widget: attached {EV_WIDGET} Current internal_shared_not_void: internal_shared /= Void -- from SD_DOCKER_SOURCE internal_shared_not_void: internal_shared /= Void note library: "SmartDocking: Library of reusable components for Eiffel." copyright: "Copyright (c) 1984-2017, 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 SD_PLACE_HOLDER_ZONE -- Generated by Eiffel Studio --
For more details: eiffel.org