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
EV_ANY
require ANY
True
ensure then 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
close_actions: EV_NEW_ITEM_ACTION_SEQUENCE
count: INTEGER_32
`Current'
count
ensure
result_valid: Result >= 0
customizeable_area_of_widget (widget: EV_WIDGET): EV_HORIZONTAL_BOX
`Result'
`widget'
`Current'`Result'
require
widget_contained: linear_representation.has (widget) or external_representation.has (widget)
ensure
result_not_void: Result /= Void
disabled_close_button_shown: BOOLEAN
disabled_minimize_button_shown: BOOLEAN
docked_in_actions: EV_NEW_ITEM_ACTION_SEQUENCE
`Current'
ensure
not_void: Result /= Void
docked_out_actions: EV_NEW_ITEM_ACTION_SEQUENCE
`Current'
ensure
not_void: Result /= Void
external_representation: ARRAYED_LIST [EV_WIDGET]
`Current'
`Current'
hide_disabled_close_button: BOOLEAN
`disable_close_button_shown'`False'
hide_disabled_minimize_button
disabled_minimize_button_shown`False'
is_item_external (a_widget: EV_WIDGET): BOOLEAN
`a_widget'`Current'
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
`a_widget'`Current'
ensure
result_consistent: Result implies maximized_tool /= Void
is_item_minimized (a_widget: EV_WIDGET): BOOLEAN
`a_widget'`Current'
require
widget_contained: linear_representation.has (a_widget)
linear_representation: ARRAYED_LIST [EV_WIDGET]
`Current'
`Current'`external_widgets'
`Current'
maximize_actions: EV_NEW_ITEM_ACTION_SEQUENCE
minimize_actions: EV_NEW_ITEM_ACTION_SEQUENCE
original_index_of_external_item (a_widget: EV_WIDGET): INTEGER_32
`Result'`a_widget'`Current'
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
show_disabled_close_button: BOOLEAN
disabled_close_button_shown`True'
show_disabled_minimize_button
disabled_minimize_button_shown`True'
top_widget_resizing: BOOLEAN
`Current'`Current'
feature {ANY}
parent: EV_CONTAINER
`Current'
EV_WIDGET
require EV_CONTAINABLE
not_destroyed: not is_destroyed
ensure then EV_WIDGET
bridge_ok: Result = implementation.parent
feature {ANY}
is_show_requested: BOOLEAN
`Current'
is_displayed
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_show_requested
feature
add_external (widget: EV_WIDGET; window: EV_WINDOW; name: STRING_GENERAL; position, an_x, a_y, a_width, a_height: INTEGER_32)
`widget'`Current'`name'`position'
`Current'`an_x'`a_y'
`a_width'`a_height'
`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)
`widget'
require
widget_not_void: widget /= Void
may_disable_close_button: linear_representation.has (widget) or is_item_external (widget)
disable_top_widget_resizing
`top_widget'`False'
ensure
not_top_resizing: top_widget_resizing = False
enable_close_button (widget: EV_WIDGET)
`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)
`widget'
require
widget_not_void: widget /= Void
may_enable_close_button: linear_representation.has (widget) or is_item_external (widget)
enable_top_widget_resizing
`top_widget'`True'
ensure
top_resizing: top_widget_resizing = True
extend (widget: EV_WIDGET; name: STRING_GENERAL)
`widget'
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)
`widget'`Current'`position'`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)
`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)
`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'`upper_box'`a_holder'
`a_holder'`lower_box'`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)
`a_widget'`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)
`a_widget'`a_height'
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)
`a_widget'`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)
`pixmap'
require
pixmap_not_void: pixmap /= Void
set_heights (heights: ARRAYED_LIST [INTEGER_32])
`heights'
require
heights_not_void: heights /= Void
set_heights_no_resize (heights: ARRAYED_LIST [INTEGER_32])
`heights'
`Current'
require
heights_not_void: heights /= Void
set_item_restore_height (a_widget: EV_WIDGET; a_height: INTEGER_32)
`a_widget'
`a_widget'
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)
`pixmap'
require
pixmap_not_void: pixmap /= Void
set_minimize_pixmap (pixmap: EV_PIXMAP)
`pixmap'
require
pixmap_not_void: pixmap /= Void
set_restore_pixmap (pixmap: EV_PIXMAP)
`pixmap'
require
pixmap_not_void: pixmap /= Void
unblock
wipe_out
`Current'
remove_implementationremove
rebuild
all_split_areas
ensure
empty: count = 0
no_external_tools: external_representation.is_empty
feature {ANY}
set_minimum_height (a_minimum_height: INTEGER_32)
`a_minimum_height'minimum_height
height`a_minimum_height'
minimum_height
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_height_positive: a_minimum_height >= 0
ensure EV_WIDGET
minimum_height_assigned: minimum_height = a_minimum_height
minimum_height_set_by_user_set: minimum_height_set_by_user
feature {ANY}
resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
feature {ANY}
height: INTEGER_32
minimum_height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.height
width: INTEGER_32
minimum_width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.width
feature {ANY}
is_destroyed: BOOLEAN
`Current'
EV_ANY
ensure 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
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
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
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)
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
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= Void and then implementation.interface = Current
default_create_called: default_create_called
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_DOCKABLE_SOURCE
parent_permits_docking: is_dockable implies parent_of_source_allows_docking
EV_COLORIZABLE
background_color_not_void: is_usable implies background_color /= Void
foreground_color_not_void: is_usable implies foreground_color /= Void
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 MULTIPLE_SPLIT_AREA