    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