indexing
	description: "[
		Eiffel Vision text component. Base class for text editing widgets.
	]"
	legal: "See notice at end of class."
	status: "See notice at end of class."
	date: "$Date: 2006-07-24 17:30:12 -0700 (Mon, 24 Jul 2006) $"
	revision: "$Revision: 61610 $"

deferred class interface
	EV_TEXT_COMPONENT


feature -- Access

	accept_cursor: EV_POINTER_STYLE
			-- `Result' is cursor displayed when the screen pointer is over a
			-- target that accepts pebble during pick and drop.
			-- (from EV_PICK_AND_DROPABLE)
		require -- from  EV_ABSTRACT_PICK_AND_DROPABLE
			True
		ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
			result_not_void: Result /= Void
		ensure then -- from EV_PICK_AND_DROPABLE
			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)

	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_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

	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

	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

	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)

	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

	selected_text: STRING_32
			-- Currently selected text.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		ensure
			bridge_ok: Result.is_equal (implementation.selected_text)

	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)

	text: STRING_32
			-- Text displayed in textable.
			-- (from EV_TEXTABLE)
		require -- from EV_TEXTABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_TEXTABLE
			bridge_ok: equal (Result, implementation.text)
			not_void: Result /= Void
			cloned: Result /= implementation.text
			no_carriage_returns: not Result.has ('%R')

	text_length: INTEGER_32
			-- Number of characters making up text.
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result.is_equal (implementation.text_length)
			result_not_negative: Result >= 0

	tooltip: STRING_32
			-- Tooltip displayed on `Current'.
			-- If `Result' is empty then no tooltip displayed.
			-- (from EV_TOOLTIPABLE)
		require -- from EV_TOOLTIPABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_TOOLTIPABLE
			bridge_ok: is_bridge_ok (Result)
			not_void: Result /= Void
			cloned: is_cloned (Result)
	
feature -- Measurement

	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_TEXT_COMPONENT): 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_TEXT_COMPONENT): 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_TEXT_COMPONENT): 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

	caret_position: INTEGER_32
			-- Current position of caret.
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.caret_position

	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

	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)

	has_selection: BOOLEAN
			-- Does current have a selection?
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.has_selection

	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_editable: BOOLEAN
			-- Is text editable?
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.is_editable

	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_in_default_state_for_tabs: BOOLEAN
			-- Default state for widgets.
			-- (from EV_TAB_CONTROLABLE)

	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

	is_tabable_from: BOOLEAN
			-- Is Current able to be tabbed from?
			-- (from EV_TAB_CONTROLABLE)
		require -- from EV_TAB_CONTROLABLE
			not_destroyed: not is_destroyed

	is_tabable_to: BOOLEAN
			-- Is Current able to be tabbed to?
			-- (from EV_TAB_CONTROLABLE)
		require -- from EV_TAB_CONTROLABLE
			not_destroyed: not is_destroyed

	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

	real_source: 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))

	selection_end: INTEGER_32
			-- Index of last character selected.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		ensure
			bridge_ok: Result = implementation.selection_end
			within_range: Result >= 1 and Result <= text_length
			consistent_with_selection_start: Result >= selection_start

	selection_start: INTEGER_32
			-- Index of first selected character.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		ensure
			bridge_ok: Result = implementation.selection_start
			within_range: Result >= 1 and Result <= text_length
			consistent_with_selection_end: selection_end >= Result

	valid_caret_position (pos: INTEGER_32): BOOLEAN
			-- Is `pos' a valid caret position?
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.valid_caret_position (pos)
	
feature -- Status setting

	center_pointer
			-- Position screen pointer over center of `Current'.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed

	disable_capture
			-- Disable grab of all user input events.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: