Automatic generation produced by ISE Eiffel

Classes Clusters Cluster hierarchy Chart Relations Flat contracts Go to:
note description: "[ This class is the main window of MEMORY ANALYZER. May the memory analyzer communicate with other program which can surround the target debugged application and send the MEMORY's memory map to a pipe? It should be nice, because it will only analyze the objects which we care. ]" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2020-12-16 11:40:15 -0900 (Wed, 16 Dec 2020) $" revision: "$Revision: 105020 $" class interface MA_WINDOW create make (a_dir: READABLE_STRING_GENERAL) -- Initialize current main memory analyzer window. require a_dir_not_void: a_dir /= Void feature -- Access accelerators: EV_ACCELERATOR_LIST -- Key combination shortcuts associated with this window. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: Result = implementation.accelerator_list not_void: Result /= Void 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 add_current: EV_BUTTON -- (from MA_WINDOW_IMP) arrange_circle: EV_BUTTON -- (from MA_WINDOW_IMP) auto_refresh: EV_TOOL_BAR_TOGGLE_BUTTON -- (from MA_WINDOW_IMP) B_add_current_state: STRING_8 -- Result is STRING constant named `b_add_current_state`. -- (from MA_CONSTANTS_IMP) B_arrange_circle: STRING_8 -- Result is STRING constant named `b_arrange_circle`. -- (from MA_CONSTANTS_IMP) B_clear_graph: STRING_8 -- Result is STRING constant named `b_clear_graph`. -- (from MA_CONSTANTS_IMP) B_clear_graph_except_selected: STRING_8 -- Result is STRING constant named `b_clear_graph_except_selected`. -- (from MA_CONSTANTS_IMP) B_filter: STRING_8 -- Result is STRING constant named `b_filter`. -- (from MA_CONSTANTS_IMP) B_find: STRING_8 -- Result is STRING constant named `b_find`. -- (from MA_CONSTANTS_IMP) B_find_referers: STRING_8 -- Result is STRING constant named `b_find_referers`. -- (from MA_CONSTANTS_IMP) B_find_tip_by_instance_name: STRING_8 -- Result is STRING constant named `b_find_tip_by_instance_name`. -- (from MA_CONSTANTS_IMP) B_find_tip_by_type: STRING_8 -- Result is STRING constant named `b_find_tip_by_type`. -- (from MA_CONSTANTS_IMP) B_show_object_changed: STRING_8 -- Result is STRING constant named `b_show_object_changed`. -- (from MA_CONSTANTS_IMP) 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)) Border_width: INTEGER_32 -- Result is INTEGER constant named border_width. -- (from MA_CONSTANTS_IMP) c_histogram: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) c_history: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) chunk_size_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) clear_graph: EV_BUTTON -- (from MA_WINDOW_IMP) coalesce_period_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) collect_statics: EV_TOOL_BAR_TOGGLE_BUTTON -- (from MA_WINDOW_IMP) collected_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) collected_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) collected_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) collected_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) collection_period_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) 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) cpu_interval_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_interval_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_interval_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_interval_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cpu_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cycle_count_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) cycle_count_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) 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 Dlg_max_height_speed: INTEGER_32 -- Result is INTEGER constant named dlg_max_height_speed. -- (from MA_CONSTANTS_IMP) Dlg_max_width_speed: INTEGER_32 -- Result is INTEGER constant named dlg_max_width_speed. -- (from MA_CONSTANTS_IMP) eiffel_histogram: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) eiffel_history: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) eiffel_view_frame: EV_FRAME -- (from MA_WINDOW_IMP) 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 filter_setting: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) find: EV_BUTTON -- (from MA_WINDOW_IMP) find_refers: EV_BUTTON -- (from MA_WINDOW_IMP) 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) gc_enable: EV_TOOL_BAR_TOGGLE_BUTTON -- (from MA_WINDOW_IMP) gc_graphs: EV_VERTICAL_BOX -- (from MA_WINDOW_IMP) gc_now: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) generating_type: TYPE [detachable MA_WINDOW] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generation_object_limit_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) 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_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 icon_name: STRING_32 -- Name displayed when `Current is minimized. -- If `is_empty` then `title` is displayed. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW bridge_ok: equal (Result, implementation.icon_name) result_not_void: Result /= Void cloned: Result /= implementation.icon_name icon_pixmap: EV_PIXMAP -- Window icon. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW bridge_ok: Result.is_equal (implementation.icon_pixmap) 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) increased_object_result: EV_GRID -- (from MA_WINDOW_IMP) 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 largest_coalesced_block_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) Lb_auto_refresh: STRING_8 -- Result is STRING constant named `lb_auto_refresh`. -- (from MA_CONSTANTS_IMP) Lb_chunk_size: STRING_8 -- Result is STRING constant named `lb_chunk_size`. -- (from MA_CONSTANTS_IMP) Lb_coalesce_period: STRING_8 -- Result is STRING constant named `lb_coalesce_period`. -- (from MA_CONSTANTS_IMP) Lb_collected: STRING_8 -- Result is STRING constant named `lb_collected`. -- (from MA_CONSTANTS_IMP) Lb_collected_average: STRING_8 -- Result is STRING constant named `lb_collected_average`. -- (from MA_CONSTANTS_IMP) Lb_collection_period: STRING_8 -- Result is STRING constant named `lb_collection_period`. -- (from MA_CONSTANTS_IMP) Lb_cpu_interval_time: STRING_8 -- Result is STRING constant named `lb_cpu_interval_time`. -- (from MA_CONSTANTS_IMP) Lb_cpu_interval_time_average: STRING_8 -- Result is STRING constant named `lb_cpu_interval_time_average`. -- (from MA_CONSTANTS_IMP) Lb_cpu_time: STRING_8 -- Result is STRING constant named `lb_cpu_time`. -- (from MA_CONSTANTS_IMP) Lb_cpu_time_average: STRING_8 -- Result is STRING constant named `lb_cpu_time_average`. -- (from MA_CONSTANTS_IMP) Lb_cycle_count: STRING_8 -- Result is STRING constant named `lb_cycle_count`. -- (from MA_CONSTANTS_IMP) Lb_generation_object_limit: STRING_8 -- Result is STRING constant named `lb_generation_object_limit`. -- (from MA_CONSTANTS_IMP) Lb_largest_coalesced_block: STRING_8 -- Result is STRING constant named `lb_largest_coalesced_block`. -- (from MA_CONSTANTS_IMP) Lb_max_memory: STRING_8 -- Result is STRING constant named `lb_max_memory`. -- (from MA_CONSTANTS_IMP) Lb_memory_threshold: STRING_8 -- Result is STRING constant named `lb_memory_threshold`. -- (from MA_CONSTANTS_IMP) Lb_memory_used: STRING_8 -- Result is STRING constant named `lb_memory_used`. -- (from MA_CONSTANTS_IMP) Lb_object_name: STRING_8 -- Result is STRING constant named `lb_object_name`. -- (from MA_CONSTANTS_IMP) Lb_objects_count: STRING_8 -- Result is STRING constant named `lb_objects_count`. -- (from MA_CONSTANTS_IMP) Lb_real_interval_time: STRING_8 -- Result is STRING constant named `lb_real_interval_time`. -- (from MA_CONSTANTS_IMP) Lb_real_interval_time_average: STRING_8 -- Result is STRING constant named `lb_real_interval_time_average`. -- (from MA_CONSTANTS_IMP) Lb_real_time: STRING_8 -- Result is STRING constant named `lb_real_time`. -- (from MA_CONSTANTS_IMP) Lb_real_time_average: STRING_8 -- Result is STRING constant named `lb_real_time_average`. -- (from MA_CONSTANTS_IMP) Lb_scavenge_zone_size: STRING_8 -- Result is STRING constant named `lb_scavenge_zone_size`. -- (from MA_CONSTANTS_IMP) Lb_speed: STRING_8 -- Result is STRING constant named `lb_speed`. -- (from MA_CONSTANTS_IMP) Lb_system_interval_time: STRING_8 -- Result is STRING constant named `lb_system_interval_time`. -- (from MA_CONSTANTS_IMP) Lb_system_interval_time_average: STRING_8 -- Result is STRING constant named `lb_system_interval_time_average`. -- (from MA_CONSTANTS_IMP) Lb_system_time: STRING_8 -- Result is STRING constant named `lb_system_time`. -- (from MA_CONSTANTS_IMP) Lb_system_time_average: STRING_8 -- Result is STRING constant named `lb_system_time_average`. -- (from MA_CONSTANTS_IMP) Lb_tenure: STRING_8 -- Result is STRING constant named `lb_tenure`. -- (from MA_CONSTANTS_IMP) Lb_typ_name: STRING_8 -- Result is STRING constant named `lb_typ_name`. -- (from MA_CONSTANTS_IMP) Lb_zoom: STRING_8 -- Result is STRING constant named `lb_zoom`. -- (from MA_CONSTANTS_IMP) main_book: EV_NOTEBOOK -- (from MA_WINDOW_IMP) Main_notebook_tab_height_minimum: INTEGER_32 -- Result is INTEGER constant named main_notebook_tab_height_minimum. -- (from MA_CONSTANTS_IMP) Main_notebook_tab_width_minimum: INTEGER_32 -- Result is INTEGER constant named main_notebook_tab_width_minimum. -- (from MA_CONSTANTS_IMP) max_memory_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) Maximum_dimension: INTEGER_32 = 32000 -- Maximum width/height that a window can be set to. -- (from EV_WINDOW) maximum_height: INTEGER_32 -- Upper bound on `height` in pixels. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: (Result = implementation.internal_maximum_height) or (Result = implementation.minimum_height) maximum_width: INTEGER_32 -- Upper bound on `width` in pixels. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: (Result = implementation.internal_maximum_width) or (Result = implementation.minimum_width) memory_spot_1: EV_GRID -- (from MA_WINDOW_IMP) memory_spot_2: EV_GRID -- (from MA_WINDOW_IMP) memory_threshold_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) memory_used_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) memory_used_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) menu_bar: detachable EV_MENU_BAR -- Horizontal bar at top of client area that contains menu's. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: Result = implementation.menu_bar Nb_memory_changed: STRING_8 -- Result is STRING constant named `nb_memory_changed`. -- (from MA_CONSTANTS_IMP) Nb_memory_statistics: STRING_8 -- Result is STRING constant named `nb_memory_statistics`. -- (from MA_CONSTANTS_IMP) Nb_object_graph: STRING_8 -- Result is STRING constant named `nb_object_graph`. -- (from MA_CONSTANTS_IMP) Nb_object_grid: STRING_8 -- Result is STRING constant named `nb_object_grid`. -- (from MA_CONSTANTS_IMP) Nb_search_route: STRING_8 -- (from MA_CONSTANTS_IMP) notebook_gc_info: EV_NOTEBOOK -- (from MA_WINDOW_IMP) object_drawing: EV_FRAME -- (from MA_WINDOW_IMP) object_grid: EV_GRID -- (from MA_WINDOW_IMP) 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 object_name_1: EV_COMBO_BOX -- (from MA_WINDOW_IMP) object_routes_panel: EV_VERTICAL_BOX -- (from MA_WINDOW_IMP) Padding_width: INTEGER_32 -- Result is INTEGER constant named padding_width. -- (from MA_CONSTANTS_IMP) 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_interval_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_interval_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_interval_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_interval_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) 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 real_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) real_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) refresh: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) refresh_speed: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) retreive: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) route_results_panel: EV_FRAME -- (from MA_WINDOW_IMP) save_datas: EV_TOOL_BAR_BUTTON -- (from MA_WINDOW_IMP) scavenge_zone_size_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) search_route_button: EV_BUTTON -- (from MA_WINDOW_IMP) Separator_width: INTEGER_32 -- Result is INTEGER constant named separator_width. -- (from MA_CONSTANTS_IMP) Shared_environment: EV_ENVIRONMENT -- Shared EV_ENVIRONMENT object. -- (from EV_SHARED_APPLICATION) show_diff_grid: EV_BUTTON -- (from MA_WINDOW_IMP) split_incre: EV_HORIZONTAL_SPLIT_AREA -- (from MA_WINDOW_IMP) split_incre_horizontal: EV_VERTICAL_SPLIT_AREA -- (from MA_WINDOW_IMP) system_interval_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_interval_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_interval_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_interval_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_time_average_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_time_average_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_time_full: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) system_time_incre: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) tab_garbage_collector_info: EV_VERTICAL_SPLIT_AREA -- (from MA_WINDOW_IMP) tab_object_graph: EV_VERTICAL_BOX -- (from MA_WINDOW_IMP) tab_object_grid: EV_VERTICAL_BOX -- (from MA_WINDOW_IMP) tab_states_compare: EV_VERTICAL_BOX -- (from MA_WINDOW_IMP) 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 Tb_add_new_class_name: STRING_8 -- Result is STRING constant named `tb_add_new_class_name`. -- (from MA_CONSTANTS_IMP) Tb_auto_refresh_enabled: STRING_8 -- Result is STRING constant named `tb_auto_refresh_enabled`. -- (from MA_CONSTANTS_IMP) Tb_collect_statics_enabled: STRING_8 -- Result is STRING constant named `tb_auto_refresh_enabled`. -- (from MA_CONSTANTS_IMP) Tb_disable_garbage_collector: STRING_8 -- Result is STRING constant named `tb_disable_garbage_collector`. -- (from MA_CONSTANTS_IMP) Tb_filter_open: STRING_8 -- Result is STRING constant named `tb_filter_open`. -- (from MA_CONSTANTS_IMP) Tb_filter_save: STRING_8 -- Result is STRING constant named `tb_filter_save`. -- (from MA_CONSTANTS_IMP) Tb_garbage_clean_now: STRING_8 -- Result is STRING constant named `tb_garbage_clean_now`. -- (from MA_CONSTANTS_IMP) Tb_open_system_states: STRING_8 -- Result is STRING constant named `tb_open_system_states`. -- (from MA_CONSTANTS_IMP) Tb_refresh_infomation: STRING_8 -- Result is STRING constant named `tb_refresh_infomation`. -- (from MA_CONSTANTS_IMP) Tb_refresh_speed_is_normal: STRING_8 -- Result is STRING constant named `tb_refresh_speed_is_normal`. -- (from MA_CONSTANTS_IMP) Tb_save_current_datas: STRING_8 -- Result is STRING constant named `tb_save_current_datas`. -- (from MA_CONSTANTS_IMP) Tb_set_analyze_filter: STRING_8 -- Result is STRING constant named `tb_set_analyze_filter`. -- (from MA_CONSTANTS_IMP) tenure_other: EV_TEXT_FIELD -- (from MA_WINDOW_IMP) title: STRING_32 -- A textual name used by the window manager. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: equal (Result, implementation.title) not_void: Result /= Void cloned: Result /= implementation.title total_histogram: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) total_history: EV_DRAWING_AREA -- (from MA_WINDOW_IMP) type_name: EV_COMBO_BOX -- (from MA_WINDOW_IMP) 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 Wnd_filter_name: STRING_8 -- Result is STRING constant named `wnd_filter_name`. -- (from MA_CONSTANTS_IMP) Wnd_memory_analyzer: STRING_8 -- Result is STRING constant named `wnd_memory_analyzer`. -- (from MA_CONSTANTS_IMP) zoom: EV_HORIZONTAL_RANGE -- (from MA_WINDOW_IMP) feature -- Access constants_initialized: BOOLEAN -- Have constants been initialized from file? -- (from MA_CONSTANTS_IMP) has_constant (a_name: STRING_8): BOOLEAN -- Does constant a_name exist? -- (from MA_CONSTANTS_IMP) require -- from MA_CONSTANTS_IMP initialized: constants_initialized name_valid: a_name /= Void and not a_name.is_empty integer_constant_by_name (a_name: STRING_8): INTEGER_32 -- Result is STRING -- (from MA_CONSTANTS_IMP) require -- from MA_CONSTANTS_IMP initialized: constants_initialized name_valid: a_name /= Void and not a_name.is_empty has_constant: has_constant (a_name) string_constant_by_name (a_name: STRING_8): detachable STRING_8 -- Result is STRING -- (from MA_CONSTANTS_IMP) require -- from MA_CONSTANTS_IMP initialized: constants_initialized name_valid: a_name /= Void and not a_name.is_empty has_constant (a_name) ensure -- from MA_CONSTANTS_IMP result_not_void: Result /= Void 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: MA_WINDOW): 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: MA_WINDOW): 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: MA_WINDOW): 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) full: BOOLEAN -- Is structure filled to capacity? -- (from EV_CELL) has (v: EV_WIDGET): BOOLEAN -- Does structure include v? -- (from EV_WINDOW) require -- from CONTAINER True ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty 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_border_enabled: BOOLEAN -- Is a border displayed around Current? -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed 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_maximized: BOOLEAN -- Is displayed at maximum size? -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW bridge_ok: Result = implementation.is_maximized is_minimized: BOOLEAN -- Is displayed iconified/minimised? -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW bridge_ok: Result = implementation.is_minimized 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)) user_can_resize: BOOLEAN -- Can the user resize? -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW bridge_ok: Result = implementation.user_can_resize 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_border -- Ensure no border is displayed around Current. -- Has no immediate effect if `user_can_resize`, although -- is reflected at next call to `disable_user_resize`. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW border_disabled: not user_can_resize implies not is_border_enabled 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 disable_user_resize -- Prevent user from resizing. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW not_user_can_resize: not user_can_resize enable_border -- Ensure a border is displayed around Current. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW is_border_enabled: is_border_enabled 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 enable_user_resize -- Allow user to resize. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW user_can_resize: user_can_resize hide -- Request that Current not be displayed even when its parent is. -- If successful, make `is_show_requested` False. -- (from EV_WINDOW) require -- from EV_WIDGET not_destroyed: not is_destroyed lock_update -- Lock drawing updates for this window on certain platforms until -- `unlock_update` is called. -- -- Note: - Only one window can be locked at a time. --       - The window cannot be moved while update is locked. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed no_locked_window: ev_application.locked_window = Void ensure -- from EV_WINDOW locked_window_is_current: ev_application.locked_window = Current lower -- Request that window be displayed below all other windows. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed maximize -- Request that Current be displayed maximized. -- If successful, make `is_show_requested` True. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW is_maximized: is_maximized 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 minimize -- Display iconified/minimised. -- It is not possible to guarantee this on some -- platform configurations. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW not_displayed: not is_displayed raise -- Request that window be displayed above all other windows -- (if `is_minimized`, window is restored). -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed 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_menu_bar -- Make `menu_bar` Void. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW menu_bar_void: menu_bar = Void remove_pebble -- Make `pebble` Void and `pebble_function` `Void, -- Removing transport. -- (from EV_PICK_AND_DROPABLE) ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE pebble_removed: pebble = Void and pebble_function = Void remove_real_source -- Ensure `real_source` is Void. -- (from EV_DOCKABLE_SOURCE) require -- from EV_DOCKABLE_SOURCE not_destroyed: not is_destroyed ensure -- from EV_DOCKABLE_SOURCE real_source_void: real_source = Void remove_real_target -- Ensure `real_target` is Void. -- (from EV_WIDGET) require -- from EV_WIDGET not_destroyed: not is_destroyed ensure -- from EV_WIDGET real_target_void: real_target = Void remove_title -- Make `title` empty. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed ensure -- from EV_WINDOW title_empty: title.is_empty restore -- Restore to original position when minimized or maximized. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW minimize_restored: old is_minimized implies not is_minimized maximize_restored: old is_maximized implies not is_maximized 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_height (a_height: INTEGER_32) -- Assign a_height to `height` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed a_height_positive_or_zero: a_height >= 0 ensure -- from EV_POSITIONABLE height_assigned: height = minimum_height or else height = a_height set_maximum_height (a_maximum_height: INTEGER_32) -- Assign a_maximum_height to `maximum_height` in pixels. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed a_maximum_height_non_negative: a_maximum_height >= 0 a_maximum_height_not_less_than_minimum_height: a_maximum_height >= minimum_height a_maximum_height_not_greater_than_maximum_dimension: a_maximum_height <= Maximum_dimension ensure -- from EV_WINDOW maximum_height_assigned: maximum_height = a_maximum_height set_maximum_size (a_maximum_width, a_maximum_height: INTEGER_32) -- Assign a_maximum_width to `maximum_width` -- and a_maximum_height to `maximum_height` in pixels. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed a_maximum_width_not_less_than_minimum_width: a_maximum_width >= minimum_width a_maximum_height_not_less_than_minimum_height: a_maximum_height >= minimum_height a_maximum_width_not_greater_than_maximum_dimension: a_maximum_width <= Maximum_dimension a_maximum_height_not_greater_than_maximum_dimension: a_maximum_height <= Maximum_dimension ensure -- from EV_WINDOW maximum_width_assigned: maximum_width = a_maximum_width maximum_height_assigned: maximum_height = a_maximum_height set_maximum_width (a_maximum_width: INTEGER_32) -- Assign a_maximum_width to `maximum_width` in pixels. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed a_maximum_width_non_negative: a_maximum_width >= 0 a_maximum_width_not_less_than_minimum_width: a_maximum_width >= minimum_width a_maximum_width_not_greater_than_maximum_dimension: a_maximum_width <= Maximum_dimension ensure -- from EV_WINDOW maximum_width_assigned: maximum_width = a_maximum_width set_menu_bar (a_menu_bar: EV_MENU_BAR) -- Assign a_menu_bar to `menu_bar`. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed no_menu_bar_assigned: menu_bar = Void a_menu_bar_not_void: a_menu_bar /= Void a_menu_bar_not_parented: a_menu_bar.parent = Void ensure -- from EV_WINDOW assigned: menu_bar = a_menu_bar 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_position (a_x, a_y: INTEGER_32) -- Assign a_x to `x_position` and a_y to `y_position` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed 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_size (a_width, a_height: INTEGER_32) -- Assign a_width to `width` and a_height to `height` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed a_width_positive_or_zero: a_width >= 0 a_height_positive_or_zero: a_height >= 0 ensure -- from EV_POSITIONABLE width_assigned: width = minimum_width or else width = a_width height_assigned: height = minimum_height or else height = a_height 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_title (a_title: separate READABLE_STRING_GENERAL) -- Assign a_title to `title`. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed a_title_not_void: a_title /= Void ensure -- from EV_WINDOW a_title_assigned: title.same_string_general (create {STRING_32}.make_from_separate (a_title) end) cloned: title /= a_title 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 set_width (a_width: INTEGER_32) -- Assign a_width to `width` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed a_width_positive_or_zero: a_width >= 0 ensure -- from EV_POSITIONABLE width_assigned: width = minimum_width or else width = a_width set_x_position (a_x: INTEGER_32) -- Assign a_x to `x_position` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed ensure -- from EV_POSITIONABLE x_position_assigned: x_position = a_x set_y_position (a_y: INTEGER_32) -- Assign a_y to `y_position` in pixels. -- (from EV_POSITIONABLE) require -- from EV_POSITIONABLE not_destroyed: not is_destroyed ensure -- from EV_POSITIONABLE y_position_assigned: y_position = a_y show -- Request that Current be displayed when its parent is. -- True by default. -- If successful, make `is_show_requested` True. -- (from EV_WINDOW) require -- from EV_WIDGET not_destroyed: not is_destroyed show_configurable_target_menu (a_x, a_y: INTEGER_32) -- Show the configurable target menu at position a_x, a_y relative to Current. -- (from EV_PICK_AND_DROPABLE) require -- from EV_PICK_AND_DROPABLE not_destroyed: not is_destroyed mode_is_configurable_target_menu: mode_is_configurable_target_menu configurable_menu_handler_set: configurable_target_menu_handler /= Void show_relative_to_window (a_parent: EV_WINDOW) -- Show Current with respect to a_parent. -- (from EV_WINDOW) require -- from EV_WINDOW not_void: a_parent /= Void not_destroyed: not is_destroyed parent_not_destroyed: not a_parent.is_destroyed a_window_not_current: a_parent /= Current unlock_update -- Unlock updates for this widget on certain platforms. -- (from EV_WINDOW) require -- from EV_WINDOW not_destroyed: not is_destroyed locked_window_is_current: ev_application.locked_window = Current ensure -- from EV_WINDOW no_locked_window: ev_application.locked_window = 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 (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 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_icon_name -- Make `icon_name` empty. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed ensure -- from EV_TITLED_WINDOW icon_name_removed: icon_name.is_empty 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)) 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_icon_name (an_icon_name: READABLE_STRING_GENERAL) -- Assign an_icon_name to `icon_name`. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed an_icon_name_not_void: an_icon_name /= Void ensure -- from EV_TITLED_WINDOW icon_name_assigned: icon_name.same_string_general (an_icon_name) cloned: icon_name /= an_icon_name set_icon_pixmap (an_icon: EV_PIXMAP) -- Assign an_icon to icon. -- (from EV_TITLED_WINDOW) require -- from EV_TITLED_WINDOW not_destroyed: not is_destroyed pixmap_not_void: an_icon /= Void ensure -- from EV_TITLED_WINDOW icon_pixmap_assigned: icon_pixmap.is_equal (an_icon) 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 (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 frozen deep_copy (other: MA_WINDOW) -- 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: MA_WINDOW -- 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: MA_WINDOW) -- 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: MA_WINDOW -- 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: MA_WINDOW -- 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 MA_WINDOW -- 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) is_in_default_state: BOOLEAN -- Is Current in its default state? -- (from MA_WINDOW_IMP) require -- from EV_ANY True feature -- Colors Decreased_color: EV_COLOR -- Color used when obejct count decreased. -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY green_color_set: Result /= Void Increased_color: EV_COLOR -- Color used when object count increased. -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY red_color_set: Result /= Void feature -- Command destroy_and_exit_if_last -- Destroy current window and destroy instance of EV_APPLICATION if -- no more top level windows remain in the system. -- (from EV_WINDOW) 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_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 -- Cursors Accept_node: EV_POINTER_STYLE -- Icon used when picking -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY accept_node_not_void: Result /= Void Accept_node_class: EV_POINTER_STYLE -- Icon used when picking -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY accept_node_class: Result /= Void Deny_node: EV_POINTER_STYLE -- Icon used when picking -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY deny_node_not_void: Result /= Void Deny_node_class: EV_POINTER_STYLE -- Icon used when picking -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY deny_node_class: Result /= Void feature -- Event handling close_request_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed whan a request to close window -- has been received. -- (from EV_WINDOW_ACTION_SEQUENCES) ensure -- from EV_WINDOW_ACTION_SEQUENCES not_void: Result /= Void conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES) require -- from EV_ABSTRACT_PICK_AND_DROPABLE True ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES not_void: Result /= Void 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 hide_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when window is hidden. -- (from EV_WINDOW_ACTION_SEQUENCES) ensure -- from EV_WINDOW_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 maximize_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when window is maximized. -- (from EV_TITLED_WINDOW_ACTION_SEQUENCES) ensure -- from EV_TITLED_WINDOW_ACTION_SEQUENCES not_void: Result /= Void minimize_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when window is minimized. -- (from EV_TITLED_WINDOW_ACTION_SEQUENCES) ensure -- from EV_TITLED_WINDOW_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 move_actions: EV_GEOMETRY_ACTION_SEQUENCE -- Actions to be performed when window moves. -- (from EV_WINDOW_ACTION_SEQUENCES) ensure -- from EV_WINDOW_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 restore_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when window leaves maximized or -- minimized state. -- (from EV_TITLED_WINDOW_ACTION_SEQUENCES) ensure -- from EV_TITLED_WINDOW_ACTION_SEQUENCES not_void: Result /= Void show_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when window is shown. -- (from EV_WINDOW_ACTION_SEQUENCES) ensure -- from EV_WINDOW_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 -- Redefine destroy -- Destroy window, clear singleton. require -- from EV_ANY True ensure -- from EV_ANY is_destroyed: is_destroyed feature -- Singletons filter: MA_FILTER_SINGLETON -- FILTER_SINGLETON instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY filter_not_void: Result /= Void filter_window: MA_FILTER_WINDOW -- FILTER_WINDOW instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY filter_window_not_void: Result /= Void Grid_util: MA_GRID_UTIL_SINGLETON -- GRID_UTIL_SINGLETON instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY grid_util_not_void: Result /= Void Icons: MA_ICONS_SINGLETON -- ICONS_SINGLETON instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY icons_not_void: Result /= Void Internal: INTERNAL -- INTERNAL instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY internal_made: Internal /= Void Memory: MEMORY -- MEMORY singleton -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY memory_not_void: Result /= Void Object_finder: MA_OBJECT_FINDER_SINGLETON -- OBJECT_FINDER_SINGLETON instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY object_finder_not_void: Result /= Void System_util: MA_SYSTEM_UTIL_SINGLETON -- SYSTEM_UTIL_SINGLETON instance -- (from MA_SINGLETON_FACTORY) ensure -- from MA_SINGLETON_FACTORY system_util_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 analyze_object_gra_not_void: analyze_object_gra /= Void increase_detector_not_void: increase_detector /= Void analyze_gc_not_void: analyze_gc /= Void analyze_object_snap_not_void: analyze_object_snap /= Void timer_not_void: timer /= Void auto_refresh_not_void: auto_refresh /= Void refresh_speed_not_void: refresh_speed /= Void main_book_not_destroyed: not main_book.is_destroyed main_book_has_tab_garbage_collector_info: main_book.has (tab_garbage_collector_info) main_book_has_tab_object_grid: main_book.has (tab_object_grid) main_book_has_tab_object_graph: main_book.has (tab_object_graph) main_book_has_tab_states_compare: main_book.has (tab_states_compare) -- from EV_TITLED_WINDOW accelerators_not_void: is_usable implies accelerators /= Void -- from EV_WINDOW consistent_horizontal_bounds: is_usable implies maximum_width >= minimum_width consistent_vertical_bounds: is_usable implies maximum_height >= minimum_height -- 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 MA_CONSTANTS_IMP all_constants_not_void: All_constants /= Void note copyright: "Copyright (c) 1984-2020, 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 MA_WINDOW
Classes Clusters Cluster hierarchy Chart Relations Flat contracts Go to:

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