indexing
	description: "Window intended for transient user interaction.%NOptionally modal. A modal dialog blocks the rest of the applicationuntil closed."
	legal: "See notice at end of class."
	status: "See notice at end of class."
	keywords: "dialog, dialogue, popup, window"
	date: "$Date: 2007-05-04 13:44:00 -0700 (Fri, 04 May 2007) $"
	revision: "$Revision: 68130 $"

class interface
	EV_DIALOG


create 
	default_create
			-- Standard creation procedure.
			-- (from EV_ANY)
		require -- from  ANY
			True
		ensure then -- from EV_ANY
			is_coupled: implementation /= Void
			is_initialized: is_initialized
			default_create_called: default_create_called
			is_in_default_state: is_in_default_state

	make_with_title (a_title: STRING_GENERAL)
			-- Initialize with `a_title'.
			-- (from EV_WINDOW)
		require -- from EV_WINDOW
			a_title_not_void: a_title /= 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
			bridge_ok: Result = implementation.accept_cursor

	actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_ABSTRACT_PICK_AND_DROPABLE]
			-- Overrides default drop target on a certain position.
			-- If `Void', `Current' will use the default drop target.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed
		ensure -- from EV_WIDGET
			bridge_ok: Result = implementation.actual_drop_target_agent

	background_color: EV_COLOR
			-- Color displayed behind foreground features.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_COLORIZABLE
			bridge_ok: Result.is_equal (implementation.background_color)

	background_pixmap: 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.pixmap = Void) or Result.is_equal (implementation.pixmap)

	blocking_window: EV_WINDOW
			-- `Result' is window `Current' is shown to if
			-- is_modal or is_relative.
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.blocking_window

	configurable_target_menu_handler: PROCEDURE [ANY, TUPLE [menu: EV_MENU; target_list: ARRAYED_LIST [EV_PND_TARGET_DATA]; source: EV_PICK_AND_DROPABLE; source_pebble: ANY]]
			-- Agent used for customizing the Pick and Drop Target Menu of `Current'.
			-- (from EV_PICK_AND_DROPABLE)

	data: ANY
			-- Arbitrary user data may be stored here.
			-- (from EV_ANY)

	default_cancel_button: EV_BUTTON
			-- Default cancel button. This is the button that
			-- is pushed if the user press the escape key or
			-- close the window using the close icon.
			-- If there is no default cancel button, the close
			-- icon is disabled.
		require
			not_destroyed: not is_destroyed

	default_identifier_name: STRING_8
			-- 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 ('.')

	default_key_processing_handler: PREDICATE [ANY, TUPLE [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

	default_push_button: EV_BUTTON
			-- Default pushed button. This is the button that
			-- is pushed if the user press the enter key unless
			-- a push button is currently focused.
		require
			not_destroyed: not is_destroyed

	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
			bridge_ok: Result = implementation.deny_cursor

	foreground_color: EV_COLOR
			-- Color of foreground features like text.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_COLORIZABLE
			bridge_ok: Result.is_equal (implementation.foreground_color)

	full_identifier_path: STRING_8
			-- 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: parent /= Void implies Result.is_equal (parent.full_identifier_path + "." + identifier_name)

	generating_type: STRING_8
			-- Name of current object's generating type
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void
			generating_type_not_empty: not Result.is_empty

	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: FUNCTION [ANY, TUPLE, 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): ?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_8
			-- 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 ('.')
			default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name)

	is_docking_enabled: BOOLEAN
			-- May `Current' be docked to?
			-- If True, `Current' will accept docking
			-- from a compatible EV_DOCKABLE_SOURCE.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			bridge_ok: Result = implementation.is_docking_enabled

	is_modal: BOOLEAN
			-- Is `Current' shown modally to another window?
			-- If `True' then `Current' must be closed before
			-- application can receive user events again?
		require
			not_destroyed: not is_destroyed

	is_relative: BOOLEAN
			-- Is `Current' shown relative to another window?
		require
			not_destroyed: not is_destroyed

	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.item

	lower_bar: EV_VERTICAL_BOX
			-- Room at bottom of window. (Example use: statusbar.)
			-- (from EV_WINDOW)
		require -- from EV_WINDOW
			not_destroyed: not is_destroyed
		ensure -- from EV_WINDOW
			bridge_ok: Result = implementation.lower_bar

	maximum_dimension: INTEGER_32 is 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)

	menu_bar: 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

	frozen object_id: INTEGER_32
			-- Unique for current object in any given session
			-- (from IDENTIFIED)
		ensure -- from IDENTIFIED
			valid_id: Result > 0 implies id_object (Result) = Current

	parent: 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: 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: FUNCTION [ANY, TUPLE, ANY]
			-- Returns data to be transported by pick and drop mechanism.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
			True
		ensure then -- from EV_PICK_AND_DROPABLE
			bridge_ok: Result = implementation.pebble_function

	pebble_positioning_enabled: BOOLEAN
			-- If `True' then pick and drop start coordinates are
			-- pebble_x_position, pebble_y_position.
			-- If `False' then pick and drop start coordinates are
			-- the pointer coordinates.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from EV_PICK_AND_DROPABLE
			not_destroyed: not is_destroyed
		ensure then -- from EV_PICK_AND_DROPABLE
			bridge_ok: Result = implementation.pebble_positioning_enabled

	pebble_x_position: INTEGER_32
			-- Initial x position for pick and drop relative to `Current'.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from EV_PICK_AND_DROPABLE
			not_destroyed: not is_destroyed
		ensure then -- from EV_PICK_AND_DROPABLE
			bridge_ok: Result = implementation.pebble_x_position

	pebble_y_position: INTEGER_32
			-- Initial y position for pick and drop relative to `Current'.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from EV_PICK_AND_DROPABLE
			not_destroyed: not is_destroyed
		ensure then -- from EV_PICK_AND_DROPABLE
			bridge_ok: Result = implementation.pebble_y_position

	pointer_position: EV_COORDINATE
			-- Position of the screen pointer relative to `Current'.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed
			is_show_requested: is_show_requested

	pointer_style: EV_POINTER_STYLE
			-- Cursor displayed when pointer is over this widget.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed

	real_target: EV_DOCKABLE_TARGET
			-- `Result' is target used during a dockable transport if
			-- mouse pointer is above `Current'.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed
		ensure -- from EV_WIDGET
			bridge_ok: Result = implementation.real_target

	target_data_function: FUNCTION [ANY, TUPLE [ANY], 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)

	target_name: STRING_GENERAL
			-- Optional textual name describing `Current' pick and drop hole.
			-- (from EV_ABSTRACT_PICK_AND_DROPABLE)

	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

	upper_bar: EV_VERTICAL_BOX
			-- Room at top of window. (Example use: toolbars.)
			-- Positioned below menu bar.
			-- (from EV_WINDOW)
		require -- from EV_WINDOW
			not_destroyed: not is_destroyed
		ensure -- from EV_WINDOW
			bridge_ok: Result = implementation.upper_bar

	veto_dock_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN]
			-- Function to determine whether current dock is allowed.
			-- If `Result' is `True', dock will be disallowed.
			-- (from EV_DOCKABLE_TARGET)
		require -- from EV_DOCKABLE_TARGET
			not_destroyed: not is_destroyed
		ensure -- from EV_DOCKABLE_TARGET
			bridge_ok: Result = implementation.veto_dock_function
	
feature -- Measurement

	client_height: INTEGER_32
			-- Height of the area available to children in pixels. 
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			bridge_ok: Result = implementation.client_height

	client_width: INTEGER_32
			-- Width of the area available to children in pixels. 
			-- (from EV_CONTAINER)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure -- from EV_CONTAINER
			bridge_ok: Result = implementation.client_width

	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 (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			shallow_implies_deep: standard_equal (some, other) implies Result
			both_or_none_void: (some = Void) implies (Result = (other = Void))
			same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
			symmetric: Result implies deep_equal (other, some)

	frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))

	frozen is_deep_equal (other: EV_DIALOG): BOOLEAN
			-- Are `Current' and `other' attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)

	is_equal (other: EV_DIALOG): 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.is_equal (Current)
			consistent: standard_is_equal (other) implies Result

	frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' 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
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))

	frozen standard_is_equal (other: EV_DIALOG): BOOLEAN
			-- Is `other' attached to an object of the same type
			-- as current object, and field-by-field identical to it?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			same_type: Result implies same_type (other)
			symmetric: Result implies other.standard_is_equal (Current)
	
feature -- Status report

	conforms_to (other: ANY): BOOLEAN
			-- Does type of current object conform to type
			-- of `other' (as per Eiffel: The Language, chapter 13)?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void

	count: INTEGER_32
			-- Number of items in `Current'.
			-- (from EV_CELL)
		require -- from EV_CONTAINER
			not_destroyed: not is_destroyed
		ensure then -- from EV_CELL
			valid_result: Result = 0 or Result = 1

	extendible: BOOLEAN
			-- Is there no element?
			-- Was declared in EV_CELL as synonym of is_empty.
			-- (from EV_CELL)

	full: BOOLEAN
			-- Is structure filled to capacity?
			-- (from EV_CELL)

	has (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)