indexing
	description: "Objects that represent a split area that will hold multiple items."
	legal: "See notice at end of class."
	status: "See notice at end of class."
	author: ""
	date: "$Date: 2006-10-04 12:00:53 -0700 (Wed, 04 Oct 2006) $"
	revision: "$Revision: 64144 $"

class interface
	MULTIPLE_SPLIT_AREA

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_set: default_create_called
			is_in_default_state: is_in_default_state

feature -- Access

	close_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- 	Actions to be performed after close icon is selected.

	count: INTEGER_32
			-- Number of widgets actually within `Current', does not include any
			-- widgets that are currently docked out. Therefore, when a widget is
			-- docked out, count is reduced by one.
		ensure
			result_valid: Result >= 0

	customizeable_area_of_widget (widget: EV_WIDGET): EV_HORIZONTAL_BOX
			-- `Result' is an EV_HORIZONTAL_BOX contained in the header of the tool
			-- surrounding `widget' which permits you to customize the tools appearence
			-- in `Current'. You should not unparent, `Result' or do anything dangerous
			-- to this widget, and it should be simply used to insert and remove
			-- widgets for customization as required.
		require
			widget_contained: linear_representation.has (widget) or external_representation.has (widget)
		ensure
			result_not_void: Result /= Void

	disabled_close_button_shown: BOOLEAN
			-- Are close buttons displayed (disabled) for widgets that may not be closed?

	disabled_minimize_button_shown: BOOLEAN
			-- Are disabled minimize buttons displayed?

	docked_in_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- Actions to be performed after a widget has been docked in to `Current'.
		ensure
			not_void: Result /= Void

	docked_out_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- Actions to be performed when a widget is docked out of `Current'.
		ensure
			not_void: Result /= Void

	external_representation: ARRAYED_LIST [EV_WIDGET]
			-- All widgets that have been inerted into `Current' but are presently
			-- docked out of `Current'. No paticular order is guaranteed.

	hide_disabled_close_button: BOOLEAN
			-- Ensure `disable_close_button_shown' is `False'.

	hide_disabled_minimize_button
			-- Ensure disabled_minimize_button_shown is `False'.

	is_item_external (a_widget: EV_WIDGET): BOOLEAN
			-- Is `a_widget' currently external to `Current'?
			-- i.e. has been docked out.
		require
			widget_not_void: a_widget /= Void
		ensure
			result_consistent: Result implies external_representation.has (a_widget)

	is_item_maximized (a_widget: EV_WIDGET): BOOLEAN
			-- Is `a_widget' maximized in `Current'?
		ensure
			result_consistent: Result implies maximized_tool /= Void

	is_item_minimized (a_widget: EV_WIDGET): BOOLEAN
			-- Is `a_widget' minimized in `Current'?
		require
			widget_contained: linear_representation.has (a_widget)

	linear_representation: ARRAYED_LIST [EV_WIDGET]
			-- All widgets held in `Current'. This only includes widgets that
			-- are not currently docked out of `Current'. See `external_widgets'
			-- for these. Ordered as displayed in `Current'.

	maximize_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- Actions to be performed after a maximize icon is selected.

	minimize_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- Actions to be performed after a minimize icon is selected.

	original_index_of_external_item (a_widget: EV_WIDGET): INTEGER_32
			-- `Result' is original index of `a_widget' in `Current' before
			-- it was made external.
		require
			widget_not_void: a_widget /= Void
			item_is_external: is_item_external (a_widget)
		ensure
			result_positive: Result >= 1

	restore_actions: EV_NEW_ITEM_ACTION_SEQUENCE
			-- Actions to be performed after an item has been restored.

	show_disabled_close_button: BOOLEAN
			-- Ensure disabled_close_button_shown is `True'.

	show_disabled_minimize_button
			-- Ensure disabled_minimize_button_shown is `True'.

	top_widget_resizing: BOOLEAN
			-- Does the top widget displayed in `Current' resize vertically as `Current' is resized?
			-- If False, the bottom widget will be resized vertically instead.
	
feature {ANY} -- Access

	parent: EV_CONTAINER
			-- Contains `Current'.
			-- (from EV_WIDGET)
		require -- from EV_CONTAINABLE
			not_destroyed: not is_destroyed
		ensure then -- from EV_WIDGET
			bridge_ok: Result = implementation.parent
	
feature {ANY} -- Status report

	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
	
feature -- Status setting

	add_external (widget: EV_WIDGET; window: EV_WINDOW; name: STRING_GENERAL; position, an_x, a_y, a_width, a_height: INTEGER_32)
			-- Add `widget' to `Current' as an external tool with name `name', a restore position of `position'
			-- for when it is returned back to `Current', and a dialog screen size and position of `an_x', `a_y',
			-- `a_width' and `a_height'. This effectively restores a tool as if it had already been dragged
			-- out of `Current'.
		require
			widget_not_void: widget /= Void
			widget_not_parented: widget.parent = Void
			window_not_void: window /= Void
			name_not_void: name /= Void
			size_valid: a_width > 0 and a_height > 0
		ensure
			added_externally: external_representation.has (widget)
			not_in_linear_rep: not linear_representation.has (widget)

	block
			--

	disable_close_button (widget: EV_WIDGET)
			-- hide the close button for `widget'.
		require
			widget_not_void: widget /= Void
			may_disable_close_button: linear_representation.has (widget) or is_item_external (widget)

	disable_top_widget_resizing
			-- Ensure `top_widget' resizing is `False'.
		ensure
			not_top_resizing: top_widget_resizing = False

	enable_close_button (widget: EV_WIDGET)
			-- Display a close button for `widget'.
		require
			widget_not_void: widget /= Void
			may_enable_close_button: linear_representation.has (widget) or is_item_external (widget)

	enable_close_button_as_grayed (widget: EV_WIDGET)
			-- Display a grayed out close button for `widget'.
		require
			widget_not_void: widget /= Void
			may_enable_close_button: linear_representation.has (widget) or is_item_external (widget)

	enable_top_widget_resizing
			-- Ensure `top_widget' resizing is `True'.
		ensure
			top_resizing: top_widget_resizing = True

	extend (widget: EV_WIDGET; name: STRING_GENERAL)
			-- Add `widget' to end with default height of 150 pixels.
		require
			widget_not_void: widget /= Void
			name_not_void: name /= Void
		ensure
			has_widget: linear_representation.has (widget)
			count_increased: linear_representation.count = old linear_representation.count + 1

	insert_widget (widget: EV_WIDGET; name: STRING_GENERAL; position, desired_height: INTEGER_32)
			-- Insert `widget' into `Current' at position `position' with height `desired_height'.
		require
			widget_not_void: widget /= Void
			position_valid: position >= 1 and position <= count + 1
			not_contained: not linear_representation.has (widget)
			name_not_void: name /= Void
		ensure
			contained: linear_representation.has (widget)
			count_increased: linear_representation.count = old linear_representation.count + 1

	is_blocked: BOOLEAN

	maximize_item (a_widget: EV_WIDGET)
			-- maximize `a_widget'.
		require
			has_widget: linear_representation.has (a_widget)
			widget_not_maximized: not is_item_maximized (a_widget)
		ensure
			is_maximized: is_item_maximized (a_widget)

	minimize_item (a_widget: EV_WIDGET)
			-- Minimize `a_widget'.
		require
			has_widget: linear_representation.has (a_widget)
			widget_not_minimized: not is_item_minimized (a_widget)
		ensure
			is_minimized: is_item_minimized (a_widget)

	place_holder_inside_insert_structure (a_holder: MULTIPLE_SPLIT_AREA_TOOL_HOLDER): EV_VERTICAL_BOX
			-- `Result' is a vertical box containing a vertical box representing `upper_box' of `a_holder',
			-- `a_holder' itself and a vertical box representing `lower_box' of `a_holder'.
		require
			holder_not_void: a_holder /= Void
		ensure
			result_not_void: Result /= Void
			result_filled_correctly: Result.count = 3 and Result.i_th (2) = a_holder

	remove (a_widget: EV_WIDGET)
			-- Remove `a_widget' from `Current'
		require
			a_widget_not_void: a_widget /= Void
			contained: linear_representation.has (a_widget) or is_item_external (a_widget)
		ensure
			remove: not linear_representation.has (a_widget)
			widget_not_parented: a_widget.parent = Void
			count_decreased: old linear_representation.has (a_widget) implies linear_representation.count = old linear_representation.count - 1

	resize_widget_to (a_widget: EV_WIDGET; a_height: INTEGER_32)
			-- Resize `a_widget' to `a_height' pixels.
		require
			widget_not_void: a_widget /= Void
			has_widget: linear_representation.has (a_widget) or is_item_external (a_widget)
			height_positive: a_height >= 0

	restore_item (a_widget: EV_WIDGET)
			-- Restore representation of `a_widget' within `Current'.
		require
			has_widget: linear_representation.has (a_widget)
			widget_maximized_or_minimized: is_item_maximized (a_widget) or is_item_minimized (a_widget)

	set_close_pixmap (pixmap: EV_PIXMAP)
			-- Use `pixmap' as image on close buttons.
		require
			pixmap_not_void: pixmap /= Void

	set_heights (heights: ARRAYED_LIST [INTEGER_32])
			-- Adjust heights of contents based on `heights'.
		require
			heights_not_void: heights /= Void

	set_heights_no_resize (heights: ARRAYED_LIST [INTEGER_32])
			-- Adjust heights of contents based on `heights' as a guide,
			-- but ensure that `Current' is not resized unless the
			-- minimum sizes of each widget force it to be so.
		require
			heights_not_void: heights /= Void

	set_item_restore_height (a_widget: EV_WIDGET; a_height: INTEGER_32)
			-- Associate a restore height with item `a_widget'.
			-- This height will be used when `a_widget' is restored from
			-- a minimized of maximized state.
		require
			has_widget: linear_representation.has (a_widget)
			widget_maximized_or_minimized: is_item_maximized (a_widget) or is_item_minimized (a_widget)
			height_valid: a_height >= 0

	set_maximize_pixmap (pixmap: EV_PIXMAP)
			-- Use `pixmap' as image on maximize buttons.
		require
			pixmap_not_void: pixmap /= Void

	set_minimize_pixmap (pixmap: EV_PIXMAP)
			-- Use `pixmap' as image on minimize buttons.
		require
			pixmap_not_void: pixmap /= Void

	set_restore_pixmap (pixmap: EV_PIXMAP)
			-- Use `pixmap' as image on restore buttons.
		require
			pixmap_not_void: pixmap /= Void

	unblock

	wipe_out
			-- Remove all items from `Current'.
			-- We have to call remove_implementation instead of remove,
			-- as do not want to call rebuild during the wipe out. This
			-- also means that we must explicitly wipe out all_split_areas
			-- ourself.
		ensure
			empty: count = 0
			no_external_tools: external_representation.is_empty
	
feature {ANY} -- Element change

	set_minimum_height (a_minimum_height: INTEGER_32)
			-- Set `a_minimum_height' in pixels to minimum_height.
			-- If height is less than `a_minimum_height', resize.
			-- From now, minimum_height is fixed and will not be changed
			-- dynamically by the application anymore.
			-- (from EV_WIDGET)
		require -- from EV_WIDGET
			not_destroyed: not is_destroyed
			a_minimum_height_positive: a_minimum_height >= 0
		ensure -- from EV_WIDGET
			minimum_height_assigned: minimum_height = a_minimum_height
			minimum_height_set_by_user_set: minimum_height_set_by_user
	
feature {ANY} -- Event handling

	resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
			-- Actions to be performed when size changes.
			-- (from EV_WIDGET_ACTION_SEQUENCES)
		ensure -- from EV_WIDGET_ACTION_SEQUENCES
			not_void: Result /= Void
	
feature {ANY} -- 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

	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
	
feature {ANY} -- Status Report

	is_destroyed: BOOLEAN
			-- Is `Current' no longer usable?
			-- (from EV_ANY)
		ensure -- from EV_ANY
			bridge_ok: Result = implementation.is_destroyed
	
invariant
	linear_representation_not_void: linear_representation /= Void
	all_holders_not_void: all_holders /= Void
	all_split_areas_not_void: all_split_areas /= Void
	stored_splitter_widths_not_void: stored_splitter_widths /= Void
	external_representation_not_void: external_representation /= Void
	minimized_states_not_void: minimized_states /= Void

		-- from EV_SPLIT_AREA
	maximum_greater_or_equal_minimum: is_usable implies minimum_split_position <= maximum_split_position
	splitter_in_valid_position_minimum: full implies split_position >= minimum_split_position
	splitter_in_valid_position_maximum: full implies split_position <= maximum_split_position

		-- from EV_CONTAINER
	client_width_within_bounds: is_usable implies client_width >= 0 and client_width <= width
	client_height_within_bounds: is_usable implies client_height >= 0 and client_height <= height
	all_radio_buttons_connected: is_usable implies all_radio_buttons_connected
	parent_of_items_is_current: is_usable implies parent_of_items_is_current
	items_unique: is_usable implies items_unique

		-- from EV_WIDGET
	pointer_position_not_void: is_usable and is_show_requested implies pointer_position /= Void
	is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested
	parent_contains_current: is_usable and then parent /= Void implies parent.has (Current)

		-- from EV_PICK_AND_DROPABLE
	user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1

		-- from EV_ANY
	is_initialized: is_initialized
	is_coupled: implementation /= Void and then implementation.interface = Current
	default_create_called: default_create_called

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

		-- from EV_DOCKABLE_SOURCE
	parent_permits_docking: is_dockable implies parent_of_source_allows_docking

		-- from EV_COLORIZABLE
	background_color_not_void: is_usable implies background_color /= Void
	foreground_color_not_void: is_usable implies foreground_color /= Void

		-- from EV_POSITIONED
	width_not_negative: is_usable implies width >= 0
	height_not_negative: is_usable implies height >= 0
	minimum_width_not_negative: is_usable implies minimum_width >= 0
	minimum_height_not_negative: is_usable implies minimum_height >= 0

indexing
	copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
		Eiffel Software
		356 Storke Road, 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 MULTIPLE_SPLIT_AREA