note
	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$"
	revision: "$Revision$"

deferred class
	EV_TEXT_COMPONENT

inherit
	EV_PRIMITIVE
		redefine
			implementation,
			is_in_default_state
		end

	EV_TEXTABLE
		redefine
			implementation,
			is_in_default_state
		end

	EV_TEXT_COMPONENT_ACTION_SEQUENCES

feature -- Access

	text_length: INTEGER
			-- Number of characters making up `text'.
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.text_length
		ensure
			bridge_ok: Result = implementation.text_length
			definition: Result = text.count
			Result_not_negative: Result >= 0
		end

	selected_text: STRING_32
			-- Currently selected text.
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.selected_text
		ensure
			bridge_ok: Result.is_equal (implementation.selected_text)
			definition: has_selection implies text.substring (start_selection, end_selection - 1).is_equal (Result)
		end

feature -- Status report

	is_editable: BOOLEAN
			-- Is `text' editable?
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.is_editable
		ensure
			bridge_ok: Result = implementation.is_editable
		end

	caret_position: INTEGER
			-- Current position of caret.
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.caret_position
		ensure
			bridge_ok: Result = implementation.caret_position
			within_range: Result >= 1 and Result <= text_length + 1
		end

	has_selection: BOOLEAN
			-- Does current have a selection?
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.has_selection
		ensure
			bridge_ok: Result = implementation.has_selection
			definition: Result implies start_selection /= end_selection
		end

	start_selection: INTEGER
			-- Caret position of the start of selected text if any,
			-- otherwise `caret_position'.
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.start_selection
		ensure
			bridge_ok: Result = implementation.start_selection
			within_range: Result >= 1 and Result <= text_length + 1
			consistent_with_selection_end: end_selection >= Result
		end

	end_selection: INTEGER
			-- Caret position of the end of selected text if any,
			-- otherwise `caret_position'.
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.end_selection
		ensure
			bridge_ok: Result = implementation.end_selection
			within_range: Result >= 1 and Result <= text_length + 1
			consistent_with_selection_start: Result >= start_selection
		end

	selection_start: INTEGER
			-- Index of first selected character.
		obsolete
			"Use `start_selection' instead. [2017-05-31]"
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		do
			Result := implementation.start_selection
		end

	selection_end: INTEGER
			-- Index of last character selected.
		obsolete
			"Use `end_selection - 1' instead. [2017-05-31]"
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		do
			Result := implementation.end_selection - 1
		end

	valid_caret_position (pos: INTEGER): BOOLEAN
			-- Is `pos' a valid caret position?
		require
			not_destroyed: not is_destroyed
		do
			Result := implementation.valid_caret_position (pos)
		ensure
			bridge_ok: Result = implementation.valid_caret_position (pos)
			within_range: Result implies (pos >= 1 and pos <= text_length + 1)
		end

feature -- Status setting

	enable_edit
			-- Make `Current' editable.
		require
			not_destroyed: not is_destroyed
		do
			implementation.set_editable (True)
		ensure
			is_editable: is_editable
		end

	disable_edit
			-- Make `Current' read-only.
		require
			not_destroyed: not is_destroyed
		do
			implementation.set_editable (False)
		ensure
			is_editable: not is_editable
		end

	set_caret_position (a_caret_position: INTEGER)
			-- Assign `a_caret_position' to `caret_position'.
		require
			not_destroyed: not is_destroyed
			valid_caret_position: a_caret_position >= 1 and a_caret_position <= text_length + 1
		do
			implementation.set_caret_position (a_caret_position)
		ensure
			caret_position_assigned: change_actions.is_empty implies caret_position = a_caret_position
		end

feature -- Element change

	insert_text (a_text: READABLE_STRING_GENERAL)
			-- Insert `a_text' to right of `caret_position'.
		require
			not_destroyed: not is_destroyed
			text_not_void: a_text /= Void
			no_carriage_returns: not a_text.has_code (('%R').natural_32_code)
		do
			implementation.insert_text (a_text)
		ensure
			text_insert_correctly: text.is_equal ((old text).substring (1,
				(old caret_position - 1)) + a_text.as_string_32 + (old text).substring
				((old caret_position), (old text.count)))
			caret_not_moved: old caret_position = caret_position
		end

	append_text (a_text: READABLE_STRING_GENERAL)
			-- Append `a_text' to `text'.
		require
			not_destroyed: not is_destroyed
			text_not_void: a_text /= Void
			no_carriage_returns: not a_text.has_code (('%R').natural_32_code)
		do
			implementation.append_text (a_text)
		ensure
			text_appended: check_text_modification (old text, a_text.as_string_32)
			caret_not_moved: old caret_position = caret_position
		end

	prepend_text (a_text: READABLE_STRING_GENERAL)
			-- Prepend `a_text' to `text'.
		require
			not_destroyed: not is_destroyed
			text_not_void: a_text /= Void
			no_carriage_returns: not a_text.has_code (('%R').natural_32_code)
		do
			implementation.prepend_text (a_text)
		ensure
			text_prepended:  text.is_equal (a_text.as_string_32 + old text)
			caret_not_moved: old caret_position = caret_position
		end

feature -- Resizing

	set_minimum_width_in_characters (nb: INTEGER)
			-- Make a minimum of `nb' of the widest character visible
			-- on one line.
		require
			not_destroyed: not is_destroyed
			valid_nb: nb > 0
		do
			implementation.set_minimum_width_in_characters (nb)
		ensure
			minimum_width_in_characters_assigned: old minimum_width <
				minimum_width implies minimum_width >=
				maximum_character_width * nb
		end

feature -- Basic operation

	select_region (a_start_character_pos, a_end_character_pos: INTEGER)
			-- Select (highlight) text between `a_start_character_pos' and `a_end_character_pos' character positions inclusive.
		require
			not_destroyed: not is_destroyed
			start_within_range: a_start_character_pos >= 1 and a_start_character_pos <= text_length
			end_within_range: a_end_character_pos >= 1 and a_end_character_pos <= text_length
		do
			implementation.select_region (a_start_character_pos, a_end_character_pos)
		ensure
			has_selection: has_selection
			selection_set: (a_start_character_pos <= a_end_character_pos implies
				start_selection = a_start_character_pos and end_selection = a_end_character_pos + 1) or
				start_selection = a_end_character_pos and end_selection = a_start_character_pos + 1
		end

	set_selection (a_start_pos, a_end_pos: INTEGER)
			-- Select (highlight) the characters between valid caret positions `a_start_pos' and `a_end_pos'.
		require
			valid_start: a_start_pos > 0 and a_start_pos <= text_length + 1
			valid_end: a_end_pos > 0 and a_end_pos <= text_length + 1
		do
			implementation.set_selection (a_start_pos, a_end_pos)
		ensure
			selection_set: a_start_pos /= a_end_pos = has_selection
			caret_set: (a_start_pos = a_end_pos) implies caret_position = a_start_pos
			selection_bounds_set: (a_start_pos <= a_end_pos implies
				(start_selection = a_start_pos and end_selection = a_end_pos)) or
				(start_selection = a_end_pos and end_selection = a_start_pos)
		end

	select_all
			-- Select all text.
		require
			not_destroyed: not is_destroyed
			positive_length: text_length > 0
		do
			implementation.select_all
		ensure
			has_selection: has_selection
			selection_start_set: start_selection = 1
			selection_end_set: end_selection = text_length + 1
		end

	deselect_all
			-- Unselect current selection.
		require
			not_destroyed: not is_destroyed
		do
			if has_selection then
				implementation.deselect_all
			end
		ensure
			not_has_selection: not has_selection
		end

	delete_selection
			-- Delete current selection.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
			is_editable: is_editable
		do
			implementation.delete_selection
		ensure
			has_no_selection: not has_selection
			selection_deleted: text.is_equal ((old text).substring
				(1, old start_selection - 1) + (old text).substring
				(old end_selection, (old text).count))
		end

	cut_selection
			-- Move `selected_text' to clipboard.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
			is_editable: is_editable
		do
			implementation.cut_selection
		ensure
			selection_in_clipboard:
				clipboard_content.is_equal (old selected_text)
			selection_cut: text.is_equal ((old text).substring
				(1, old start_selection - 1) + (old text).substring
				(old end_selection, (old text).count))
		end

	copy_selection
			-- Copy `selected_text' to clipboard.
		require
			not_destroyed: not is_destroyed
			has_selection: has_selection
		do
			implementation.copy_selection
		ensure
			selection_copied: clipboard_content.is_equal (selected_text)
			text_unchanged: text.is_equal (old text)
			caret_not_moved: caret_position = old caret_position
		end

	paste (a_position: INTEGER)
			-- Insert text from `clipboard' at `a_position'.
			-- No effect if clipboard is empty.
		require
			not_destroyed: not is_destroyed
			a_position_within_range:
				a_position >= 1 and a_position <= text_length + 1
			is_editable: is_editable
		do
			implementation.paste (a_position)
		ensure
			text_pasted_correctly: text.is_equal ((old text).substring (1,
				a_position - 1) + clipboard_content + ((old text).substring (
				a_position, ((old text).count))))
			caret_position_consistent:
				old caret_position <= a_position implies
					caret_position = old caret_position
			caret_position_consistent:
				old caret_position > a_position implies
				caret_position = old caret_position + clipboard_content.count
		end

feature {NONE} -- Contract support

	maximum_character_width: INTEGER
			-- Maximum width of a single character in `Current'.
		do
			Result := implementation.maximum_character_width
		end

	clipboard_content: STRING_32
			-- `Result' is contents of the clipboard.
		do
			Result := implementation.clipboard_content
		end

	check_text_modification (old_text, added_text: STRING_32): BOOLEAN
			-- Ensure that `text' is equal to `old_text' + `added_text' with
			-- all %R removed.
		do
			added_text.prune_all ('%R')
			Result := text.is_equal (old_text + added_text)
		end

	is_in_default_state: BOOLEAN
			-- Is `Current' in its default state?
		do
			Result := Precursor {EV_PRIMITIVE} and text.is_empty and
				is_editable and caret_position = 1 and not has_selection
		end

feature {EV_ANY, EV_ANY_I} -- Implementation

	implementation: EV_TEXT_COMPONENT_I
			-- Responsible for interaction with native graphics
			-- toolkit.

invariant

note
	copyright:	"Copyright (c) 1984-2015, 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 EV_TEXT_COMPONENT