indexing
	description: "This class processes the scroll messages associated to a window."
	status: "See notice at end of class."
	date: "$Date$"
	revision: "$Revision$"

class interface
	WEL_SCROLLER

create 

	make (a_window: WEL_COMPOSITE_WINDOW; horizontal_size, vertical_size, line, page: INTEGER)
			-- Make a scroller associated to a_window using
			-- horizontal_size and vertical_size as the
			-- size of the scrollable area. line and page
			-- specify the scroll incrementation for a line and
			-- a page.
		require
			a_window_not_void: a_window /= void
			a_window_exists: a_window.exists
			positive_horizontal_size: horizontal_size > 0
			positive_vertical_size: vertical_size > 0
			positive_line: line >= 0
			valid_line: line < horizontal_size and then line < vertical_size
			positive_page: page >= 0
			valid_page: page < horizontal_size and then page < vertical_size
		ensure
			window_set: window = a_window

	make_with_options (a_window: WEL_COMPOSITE_WINDOW; a_minimal_horizontal_position, a_maximal_horizontal_position, a_minimal_vertical_position, a_maximal_vertical_position, a_horizontal_line, a_horizontal_page, a_vertical_line, a_vertical_page: INTEGER)
			-- Make a scroller associated to a_window.
			-- a_minimal_horizontal_position and
			-- a_maximal_horizontal_position specify the
			-- horizontal scroll range.
			-- a_minimal_vertical_position and
			-- a_maximal_vertical_position specify the
			-- vertical scroll range.
			-- a_horizontal_line and a_horizontal_page specify
			-- the scroll incrementation for a horizontal line and
			-- page.
			-- a_vertical_line and a_vertical_page specify
			-- the scroll incrementation for a vertical line and
			-- page.
		require
			a_window_not_void: a_window /= void
			a_window_exists: a_window.exists
			consistent_horizontal_range: a_minimal_horizontal_position < a_maximal_horizontal_position
			consistent_vertical_range: a_minimal_vertical_position < a_maximal_vertical_position
			positive_horizontal_line: a_horizontal_line >= 0
			positive_vertical_line: a_vertical_line >= 0
			positive_horizontal_page: a_horizontal_page >= 0
			positive_vertical_page: a_vertical_page >= 0
		ensure
			window_set: window = a_window
			minimal_horizontal_position_set: minimal_horizontal_position = a_minimal_horizontal_position
			maximal_horizontal_position_set: maximal_horizontal_position = a_maximal_horizontal_position
			minimal_vertical_position_set: minimal_vertical_position = a_minimal_vertical_position
			maximal_vertical_position_set: maximal_vertical_position = a_maximal_vertical_position

feature -- Initialization

	make (a_window: WEL_COMPOSITE_WINDOW; horizontal_size, vertical_size, line, page: INTEGER)
			-- Make a scroller associated to a_window using
			-- horizontal_size and vertical_size as the
			-- size of the scrollable area. line and page
			-- specify the scroll incrementation for a line and
			-- a page.
		require
			a_window_not_void: a_window /= void
			a_window_exists: a_window.exists
			positive_horizontal_size: horizontal_size > 0
			positive_vertical_size: vertical_size > 0
			positive_line: line >= 0
			valid_line: line < horizontal_size and then line < vertical_size
			positive_page: page >= 0
			valid_page: page < horizontal_size and then page < vertical_size
		ensure
			window_set: window = a_window

	make_with_options (a_window: WEL_COMPOSITE_WINDOW; a_minimal_horizontal_position, a_maximal_horizontal_position, a_minimal_vertical_position, a_maximal_vertical_position, a_horizontal_line, a_horizontal_page, a_vertical_line, a_vertical_page: INTEGER)
			-- Make a scroller associated to a_window.
			-- a_minimal_horizontal_position and
			-- a_maximal_horizontal_position specify the
			-- horizontal scroll range.
			-- a_minimal_vertical_position and
			-- a_maximal_vertical_position specify the
			-- vertical scroll range.
			-- a_horizontal_line and a_horizontal_page specify
			-- the scroll incrementation for a horizontal line and
			-- page.
			-- a_vertical_line and a_vertical_page specify
			-- the scroll incrementation for a vertical line and
			-- page.
		require
			a_window_not_void: a_window /= void
			a_window_exists: a_window.exists
			consistent_horizontal_range: a_minimal_horizontal_position < a_maximal_horizontal_position
			consistent_vertical_range: a_minimal_vertical_position < a_maximal_vertical_position
			positive_horizontal_line: a_horizontal_line >= 0
			positive_vertical_line: a_vertical_line >= 0
			positive_horizontal_page: a_horizontal_page >= 0
			positive_vertical_page: a_vertical_page >= 0
		ensure
			window_set: window = a_window
			minimal_horizontal_position_set: minimal_horizontal_position = a_minimal_horizontal_position
			maximal_horizontal_position_set: maximal_horizontal_position = a_maximal_horizontal_position
			minimal_vertical_position_set: minimal_vertical_position = a_minimal_vertical_position
			maximal_vertical_position_set: maximal_vertical_position = a_maximal_vertical_position
	
feature -- Access

	horizontal_line: INTEGER
			-- Number of horizontal scroll units per line

	horizontal_page: INTEGER
			-- Number of scroll units per page
		require
			window_exists: window.exists

	horizontal_position: INTEGER
			-- Current position of the horizontal scroll box
		require
			window_exists: window.exists

	maximal_horizontal_position: INTEGER
			-- Maxium position of the horizontal scroll box
		require
			window_exists: window.exists

	maximal_vertical_position: INTEGER
			-- Maxium position of the vertical scroll box
		require
			window_exists: window.exists

	minimal_horizontal_position: INTEGER
			-- Minimum position of the horizontal scroll box
		require
			window_exists: window.exists

	minimal_vertical_position: INTEGER
			-- Minimum position of the vertical scroll box
		require
			window_exists: window.exists

	vertical_line: INTEGER
			-- Number of vertical scroll units per line

	vertical_page: INTEGER
			-- Number of scroll units per page
		require
			window_exists: window.exists

	vertical_position: INTEGER
			-- Current position of the vertical scroll box
		require
			window_exists: window.exists

	window: WEL_COMPOSITE_WINDOW
			-- Window which has the scroller
	
feature -- Element change

	set_horizontal_line (unit: INTEGER)
			-- Set horizontal_line with unit.
		require
			positive_unit: unit >= 0
		ensure
			horizontal_line_set: horizontal_line = unit

	set_horizontal_page (page_magnitude: INTEGER)
			-- Set horizontal_page with unit.
		require
			window_exists: window.exists
			positive_unit: page_magnitude >= 0
		ensure
			horizontal_page_set: horizontal_page = page_magnitude

	set_horizontal_position (position: INTEGER)
			-- Set horizontal_position with position.
		require
			window_exists: window.exists
			position_small_enough: position <= maximal_horizontal_position
			position_large_enough: position >= minimal_horizontal_position
		ensure
			horizontal_position_set: horizontal_position = position

	set_horizontal_range (minimum, maximum: INTEGER)
			-- Set horizontal_minimum_range and
			-- horizontal_maximal_range with minimum and
			-- maximum.
		require
			window_exists: window.exists
			consistent_range: minimum <= maximum
		ensure
			horizontal_minimum_range_set: minimal_horizontal_position = minimum
			horizontal_maximal_range_set: maximal_horizontal_position = maximum

	set_vertical_line (unit: INTEGER)
			-- Set vertical_line with unit.
		require
			positive_unit: unit >= 0
		ensure
			vertical_line_set: vertical_line = unit

	set_vertical_page (page_magnitude: INTEGER)
			-- Set vertical_page with unit.
		require
			window_exists: window.exists
			positive_unit: page_magnitude >= 0
		ensure
			vertical_page_set: vertical_page = page_magnitude

	set_vertical_position (position: INTEGER)
			-- Set vertical_position with position.
		require
			window_exists: window.exists
			position_small_enough: position <= maximal_vertical_position
			position_large_enough: position >= minimal_vertical_position
		ensure
			vertical_position_set: vertical_position = position

	set_vertical_range (minimum, maximum: INTEGER)
			-- Set minimal_vertical_position and
			-- maximal_vertical_position with minimum and
			-- maximum.
		require
			window_exists: window.exists
			consistent_range: minimum <= maximum
		ensure
			minimal_vertical_position_set: minimal_vertical_position = minimum
			maximal_vertical_position_set: maximal_vertical_position = maximum
	
feature -- Basic operations

	horizontal_update (inc, position: INTEGER)
			-- Update the window and the horizontal scroll box with
			-- inc and position.
		require
			window_exists: window.exists
			position_small_enough: position <= maximal_horizontal_position
			position_large_enough: position >= minimal_horizontal_position
		ensure
			horizontal_position_set: horizontal_position = position

	on_horizontal_scroll (scroll_code, pos: INTEGER)
			-- Scroll the window horizontaly.
		require
			window_exists: window.exists

	on_vertical_scroll (scroll_code, pos: INTEGER)
			-- Scroll the window verticaly.
		require
			window_exists: window.exists

	vertical_update (inc, position: INTEGER)
			-- Update the window and the vertical scroll box with
			-- inc and position.
		require
			window_exists: window.exists
			position_small_enough: position <= maximal_vertical_position
			position_large_enough: position >= minimal_vertical_position
		ensure
			vertical_position_set: vertical_position = position
	
invariant

	window_not_void: window /= void
	horizontal_position_small_enough: window.exists implies horizontal_position <= maximal_horizontal_position
	horizontal_position_large_enough: window.exists implies horizontal_position >= minimal_horizontal_position
	vertical_position_small_enough: window.exists implies vertical_position <= maximal_vertical_position
	vertical_position_large_enough: window.exists implies vertical_position >= minimal_vertical_position
	consistent_horizontal_range: window.exists implies minimal_horizontal_position <= maximal_horizontal_position
	consistent_vertical_range: window.exists implies minimal_vertical_position <= maximal_vertical_position
	positive_horizontal_line: horizontal_line >= 0
	positive_vertical_line: vertical_line >= 0
	positive_horizontal_page: horizontal_page >= 0
	positive_vertical_page: vertical_page >= 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class WEL_SCROLLER