indexing

	description: "[

		A widget where the user can slide a bar to select a value in an interval.
		
		The slider can be horizontal or vertical either by creating it with the
		appropriate creator or by calling `set_horizontal' or `set_vertical' after
		creation.
		
		The lower value of the interval has to be strictly smaller than the greater value.
		
		Events:
			- `position_changed_event': Triggered when slider position changed. Passes new value as argument.
		
		Delegate:
		EM_SLIDER_DELEGATE - A slider has a special delegate to map mouse coordinates to slider values.

	]"
	date: "$Date$"
	revision: "$Revision$"

class EM_SLIDER

inherit

	EM_WIDGET
		redefine
			delegate,
			make_void_surface
		end

create

	make_vertical,
	make_horizontal,
	make_from_range_horizontal,
	make_from_range_vertical

feature {NONE} -- Initialisation

	make_vertical is
			-- Initialise `Current' as vertical scrollbar.
			-- Range will be set to [0, 100]
		do
			make_from_range_vertical (0, 100)
		end

	make_horizontal is
			-- Initialise `Current' as horizontal scrollbar.
			-- Range will be set to [0, 100]
		do
			make_from_range_horizontal (0, 100)
		end

	make_from_range_horizontal (a_left_value, a_right_value: INTEGER) is
			-- Initialise the slider with a `a_left_value' and `a_right_value'.
		require
			valid_range: a_left_value < a_right_value
		do
			make_void_surface

			left_value := a_left_value
			right_value := a_right_value
			current_value := left_value

			is_vertical := False
			resize_to_optimal_dimension
		ensure
			left_value_set: left_value = a_left_value
			right_value_set: right_value = a_right_value
			current_value_is_left: current_value = left_value
		end

	make_from_range_vertical (a_left_value, a_right_value: INTEGER) is
			-- Initialise the slider with a `a_left_value' and `a_right_value'.
		require
			valid_range: a_left_value < a_right_value
		do
			make_void_surface

			left_value := a_left_value
			right_value := a_right_value
			current_value := left_value

			is_vertical := True
			resize_to_optimal_dimension
		ensure
			left_value_set: left_value = a_left_value
			right_value_set: right_value = a_right_value
			current_value_is_left: current_value = left_value
		end

	make_void_surface is
			-- Initialise default values.
		do
			create position_changed_event
			left_value := 0
			right_value := 100

			Precursor {EM_WIDGET}
			set_keyboard_sensitive (True)

			mouse_button_down_event.subscribe (agent handle_mouse_button_down)
			mouse_dragged_event.subscribe (agent handle_mouse_dragged)
			key_down_event.subscribe (agent handle_key_down)
		end

	delegate_factory: FUNCTION [ANY, TUPLE [], like delegate] is
			-- Factory to create default delegate
		do
			Result := theme_delegates.slider_delegate_factory
		end

feature -- Access

	delegate: EM_SLIDER_DELEGATE
			-- Delegate

	left_value: INTEGER
			-- Value if slider at left edge

	right_value: INTEGER
			-- Value if slider at right edge

	current_value: INTEGER
			-- Value at current position

feature -- Status report

	is_vertical: BOOLEAN
			-- Is `Current' displayed vertical?

	is_horizontal: BOOLEAN is
			-- Is `Current' displayed horizontal?
		do
			Result := not is_vertical
		end

feature -- Status setting

	set_vertical is
			-- Set `Current' to be vertical.
		do
			is_vertical := True
			set_changed
		ensure
			chaged: is_changed
		end

	set_horizontal is
			-- Set `Current' to be horizontal.
		do
			is_vertical := False
			set_changed
		ensure
			changed: is_changed
		end

feature -- Element change

	set_current_value (a_value: like current_value) is
			-- Set `current_value' to `a_value'.
		require
			a_value_in_range: left_value <= a_value and a_value <= right_value
		do
			current_value := a_value
			set_changed
			Component_event_queue.add_event (position_changed_event, [current_value])
		ensure
			current_value_set: current_value = a_value
			changed: is_changed
		end

	set_left_value (a_value: like left_value) is
			-- Set `left_value' to `a_value'.
		require
			a_value_valid: a_value < right_value
		do
			left_value := a_value
			if current_value < left_value then
				current_value := left_value
			end
			set_changed
		ensure
			left_value_set: left_value = a_value
			current_value_reset: old current_value < left_value implies current_value = left_value
			changed: is_changed
		end

	set_right_value (a_value: like right_value) is
			-- Set `right_value' to `a_value'.
		require
			a_value_valid: a_value > left_value
		do
			right_value := a_value
			if current_value > right_value then
				current_value := right_value
			end
			set_changed
		ensure
			right_value_set: right_value = a_value
			current_value_reset: old current_value > right_value implies current_value = right_value
			changed: is_changed
		end

	set_range (a_left_value: like left_value; a_right_value: like right_value) is
			-- Set range to `a_left_value' `a_right_value'.
		require
			valid_range: a_left_value < a_right_value
		do
			left_value := a_left_value
			right_value := a_right_value
			if current_value < left_value then
				current_value := left_value
			end
			if current_value > right_value then
				current_value := right_value
			end
			set_changed
		ensure
			left_value_set: left_value = a_left_value
			right_value_set: right_value = a_right_value
			current_value_reset: old current_value < left_value implies current_value = left_value
			current_value_reset: old current_value > right_value implies current_value = right_value
			changed: is_changed
		end

feature -- Events

	position_changed_event: EM_EVENT_CHANNEL [TUPLE [INTEGER]]
			-- Slider changed event
			-- Argument is 'current_value'

feature {NONE} -- Mouse management

	handle_mouse_button_down (event: EM_MOUSEBUTTON_EVENT) is
			-- Handle mouse down event.
		local
			new_value: INTEGER
		do
			new_value := delegate.position_to_value (Current, event.x, event.y)
			if left_value <= new_value and new_value <= right_value then
				set_current_value (new_value)
			end
		end

	handle_mouse_dragged (event: EM_MOUSEMOTION_EVENT) is
			-- Handle mouse motion event.
		local
			new_value: INTEGER
		do
			new_value := delegate.position_to_value (Current, event.x, event.y)
			if left_value <= new_value and new_value <= right_value then
				set_current_value (new_value)
			end
		end

	handle_key_down (event: EM_KEYBOARD_EVENT) is
			-- Handle key down event.
		do
			if event.key = event.sdlk_left and current_value > left_value then
				set_current_value (current_value - 1)
			elseif event.key = event.sdlk_right and current_value < right_value then
				set_current_value (current_value + 1)
			elseif event.key = event.sdlk_home then
				set_current_value (left_value)
			elseif event.key = event.sdlk_end then
				set_current_value (right_value)
			end
		end

invariant

	position_changed_event_not_void: position_changed_event /= Void
	valid_range: left_value < right_value
	valid_value: left_value <= current_value and current_value <= right_value
	vertical_xor_horizontal: is_vertical xor is_horizontal

end