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: