indexing
description: "[
An EV_FIGURE_WORLD_CELL is an EV_CELL with scrollbars displaying
world in the cell. Whenever the world does not fit into the frame
the scrolling area is resized to make sure that every part of the world
is reachable through the scrollbars. If a figure is moved closer to the
frame border then autoscroll_border the frame starts to scroll.
If the user clicks into the frame but not onto a figure the frame can
be moved arround with the "hand". A buffer is used to prefend flickering.
The buffer size as well as the drawing_area size is constant no matter
how large the world is.
example:
create figure_world_cell.make_with_world (create EV_FIGURE_WORLD)
figure_world_cell.world.extend (create {EV_FIGURE_LINE}.make_with_positions (0, 0, 100, 100))
horizontal_box.extend (figure_world_cell)
]"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
EV_MODEL_WORLD_CELL
create
make_with_world (a_world: like world)
`a_world'
require
a_world_not_void: a_world /= Void
ensure
world_set: world = a_world
feature
accept_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor
actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_ABSTRACT_PICK_AND_DROPABLE]
`Void'`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.actual_drop_target_agent
autoscroll_border: INTEGER_32
background_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.background_color)
background_pixmap: EV_PIXMAP
`Result'`Current'
`Current'
EV_CONTAINER
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
bridge_ok: (Result = Void and implementation.background_pixmap = Void) or Result.is_equal (implementation.background_pixmap)
data: ANY
EV_ANY
default_key_processing_handler: PREDICATE [ANY, TUPLE [EV_KEY]] assign set_default_key_processing_handler
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.default_key_processing_handler
deny_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor
drawing_area: EV_DRAWING_AREA
world
ev_application: EV_APPLICATION
EV_SHARED_APPLICATION
ensure EV_SHARED_APPLICATION
result_not_void: Result /= Void
foreground_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.foreground_color)
generating_type: STRING_8
ANY
generator: STRING_8
ANY
has (v: EV_WIDGET): BOOLEAN
`Current'`v'
EV_CELL
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
has_recursive (an_item: like item): BOOLEAN
`an_item'
`an_item'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
help_context: FUNCTION [ANY, TUPLE, EV_HELP_CONTEXT]
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
ensure EV_HELP_CONTEXTABLE
bridge_ok: Result = implementation.help_context
horizontal_scrollbar: EV_HORIZONTAL_SCROLL_BAR
frozen id_object (an_id: INTEGER_32): IDENTIFIED
`an_id'
IDENTIFIED
ensure IDENTIFIED
consistent: Result = Void or else Result.object_id = an_id
is_docking_enabled: BOOLEAN
`Current'
`Current'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
bridge_ok: Result = implementation.is_docking_enabled
item: EV_WIDGET
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
readable: readable
ensure EV_CONTAINER
bridge_ok: Result = implementation.item
frozen object_id: INTEGER_32
IDENTIFIED
ensure IDENTIFIED
valid_id: id_object (Result) = Current
parent: EV_CONTAINER
`Current'
EV_WIDGET
require EV_CONTAINABLE
not_destroyed: not is_destroyed
ensure then EV_WIDGET
bridge_ok: Result = implementation.parent
pebble: ANY
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble
pebble_function: FUNCTION [ANY, TUPLE, ANY]
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_function
pebble_positioning_enabled: BOOLEAN
`True'
pebble_x_positionpebble_y_position
`False'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_positioning_enabled
pebble_x_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position
pebble_y_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_y_position
pointer_position: EV_COORDINATE
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_show_requested: is_show_requested
pointer_style: EV_POINTER_STYLE
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
process_events_and_idle
`process_events'`idle_actions'Ev_application
EV_SHARED_APPLICATION
projector: EV_MODEL_BUFFER_PROJECTOR
world
real_target: EV_DOCKABLE_TARGET
`Result'
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.real_target
scroll_speed: REAL_64
autoscroll_border
target_name: STRING_GENERAL
`Current'
EV_ABSTRACT_PICK_AND_DROPABLE
vertical_scrollbar: EV_VERTICAL_SCROLL_BAR
veto_dock_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN]
`Result'`True'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
bridge_ok: Result = implementation.veto_dock_function
world: EV_MODEL_WORLD
`Current'
world_border: INTEGER_32
feature
client_height: INTEGER_32
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
bridge_ok: Result = implementation.client_height
client_width: INTEGER_32
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
bridge_ok: Result = implementation.client_width
screen_x: INTEGER_32
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.screen_x
screen_y: INTEGER_32
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.screen_y
feature
frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies some.same_type (other)
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
count: INTEGER_32
`Current'
EV_CELL
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure then EV_CELL
valid_result: Result = 0 or Result = 1
extendible: BOOLEAN
EV_CELLis_empty
EV_CELL
full: BOOLEAN
EV_CELL
has_capture: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_capture
has_focus: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_focus
frozen id_freed: BOOLEAN
`Current'
IDENTIFIED
is_autoscroll_enabled: BOOLEAN
is_displayed: BOOLEAN
`Current'
`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_displayed
is_dockable: BOOLEAN
`Current'
`True'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_dockable
is_empty: BOOLEAN
EV_CELLextendible
EV_CELL
is_external_docking_enabled: BOOLEAN
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_enabled
is_external_docking_relative: BOOLEAN
`Current'
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_relative
is_inserted (v: EV_WIDGET): BOOLEAN
`v'
`has (v)'
COLLECTION
is_resize_enabled: BOOLEAN
is_scrollbar_enabled: BOOLEAN
is_sensitive: BOOLEAN
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
bridge_ok: Result = implementation.user_is_sensitive
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
merged_radio_button_groups: ARRAYED_LIST [EV_CONTAINER]
`Result'
`Current'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
not_is_empty: Result /= Void implies not Result.is_empty
mode_is_drag_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_drag_and_drop
mode_is_pick_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_pick_and_drop
mode_is_target_menu: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_target_menu
prunable: BOOLEAN
EV_CELL
readable: BOOLEAN
EV_CELL
require EV_CONTAINER
not_destroyed: not is_destroyed
real_source: EV_DOCKABLE_SOURCE
`Result'
`Current'
`Void'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.real_source
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
writable: BOOLEAN
EV_CELL
require EV_CONTAINER
not_destroyed: not is_destroyed
feature
center_pointer
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
disable_capture
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
not_has_capture: not has_capture
disable_dockable
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
not_is_dockable: not is_dockable
disable_docking
is_docking_enabled
`Current'
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
not_dockable: not is_docking_enabled
disable_external_docking
`False'is_external_docking_enabled
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
ensure EV_DOCKABLE_SOURCE
not_externally_dockable: not is_external_docking_enabled
disable_external_docking_relative
`False'is_external_docking_relative
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
external_docking_enabled: is_external_docking_enabled
ensure EV_DOCKABLE_SOURCE
external_docking_not_relative: not is_external_docking_relative
disable_pebble_positioning
`False'pebble_positioning_enabled
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_positioning_updated: not pebble_positioning_enabled
disable_resize
is_resize_enabled
ensure
set: is_resize_enabled = False
disable_scrollbars
ensure
hide: not horizontal_scrollbar.is_show_requested and not vertical_scrollbar.is_show_requested
set: not is_scrollbar_enabled
disable_sensitive
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
is_unsensitive: not is_sensitive
enable_capture
disable_capture
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure EV_WIDGET
has_capture: has_capture
enable_dockable
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
is_dockable: is_dockable
enable_docking
is_docking_enabled
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_TARGET
is_dockable: is_docking_enabled
enable_external_docking
`True'is_external_docking_enabled
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
ensure EV_DOCKABLE_SOURCE
is_externally_dockable: is_external_docking_enabled
enable_external_docking_relative
`True'is_external_docking_relative
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
external_docking_enabled: is_external_docking_enabled
ensure EV_DOCKABLE_SOURCE
external_docking_not_relative: is_external_docking_relative
enable_pebble_positioning
`True'pebble_positioning_enabled
pebble_x_positionpebble_y_position
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_positioning_updated: pebble_positioning_enabled
enable_resize
is_resize_enabled
ensure
set: is_resize_enabled = True
enable_scrollbars
ensure
show: horizontal_scrollbar.is_show_requested and vertical_scrollbar.is_show_requested
set: is_scrollbar_enabled
enable_sensitive
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
is_sensitive: (parent = Void or parent_is_sensitive) implies is_sensitive
hide
`Current'
is_show_requested`False'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
merge_radio_button_groups (other: EV_CONTAINER)
`Current'`other'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
other_not_void: other /= Void
remove_default_key_processing_handler
default_key_processing_handler
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
default_key_processing_handler_removed: default_key_processing_handler = Void
remove_pebble
pebble`Void'pebble_function
EV_PICK_AND_DROPABLE
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_removed: pebble = Void and pebble_function = Void
remove_real_source
real_source`Void'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
real_source_void: real_source = Void
remove_real_target
real_target`Void'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
real_target_void: real_target = Void
set_accept_cursor (a_cursor: like accept_cursor)
`a_cursor'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_cursor_not_void: a_cursor /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
accept_cursor_assigned: accept_cursor.is_equal (a_cursor)
set_actual_drop_target_agent (an_agent: like actual_drop_target_agent)
`an_agent'actual_drop_target_agent
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
an_agent_not_void: an_agent /= Void
ensure EV_WIDGET
assigned: actual_drop_target_agent = an_agent
set_default_colors
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
set_default_key_processing_handler (a_handler: like default_key_processing_handler)
default_key_processing_handler`a_handler'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
set_deny_cursor (a_cursor: like deny_cursor)
`a_cursor'
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_cursor_not_void: a_cursor /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
deny_cursor_assigned: deny_cursor.is_equal (a_cursor)
set_drag_and_drop_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
drag_and_drop_set: mode_is_drag_and_drop
set_focus
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
is_sensitive: is_sensitive
set_pebble (a_pebble: like pebble)
`a_pebble'pebble
set_pebble_function
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_pebble_not_void: a_pebble /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_assigned: pebble = a_pebble
set_pebble_function (a_function: FUNCTION [ANY, TUPLE, ANY])
`a_function'pebble
pebble
`a_function'
set_pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_function_not_void: a_function /= Void
a_function_takes_two_integer_open_operands: a_function.valid_operands ([1, 1])
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_function_assigned: pebble_function = a_function
set_pebble_position (a_x, a_y: INTEGER_32)
`Current'
`True'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y
set_pick_and_drop_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
pick_and_drop_set: mode_is_pick_and_drop
set_real_source (dockable_source: EV_DOCKABLE_SOURCE)
`dockable_source'real_source
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
is_dockable: is_dockable
dockable_source_not_void: dockable_source /= Void
dockable_source_is_parent_recursive: source_has_current_recursive (dockable_source)
ensure EV_DOCKABLE_SOURCE
real_source_assigned: real_source = dockable_source
set_real_target (a_target: EV_DOCKABLE_TARGET)
`a_target'real_target
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
target_not_void: a_target /= Void
ensure EV_WIDGET
assigned: real_target = a_target
set_target_menu_mode
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure EV_PICK_AND_DROPABLE
target_menu_mode_set: mode_is_target_menu
set_target_name (a_name: STRING_GENERAL)
`a_name'target_name
EV_ABSTRACT_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
a_name_not_void: a_name /= Void
ensure EV_ABSTRACT_PICK_AND_DROPABLE
target_name_assigned: a_name /= target_name and a_name.is_equal (target_name)
set_veto_dock_function (a_function: FUNCTION [ANY, TUPLE [EV_DOCKABLE_SOURCE], BOOLEAN])
`a_function'veto_dock_function
EV_DOCKABLE_TARGET
require EV_DOCKABLE_TARGET
not_destroyed: not is_destroyed
a_function_not_void: a_function /= Void
ensure EV_DOCKABLE_TARGET
veto_function_set: veto_dock_function = a_function
show
`Current'
`True'
is_show_requested`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
unmerge_radio_button_groups (other: EV_CONTAINER)
`other'`Current'
`other'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
other_is_merged: merged_radio_button_groups.has (other)
ensure EV_CONTAINER
other_not_merged: other.merged_radio_button_groups = Void
not_contained_in_this_group: merged_radio_button_groups /= Void implies not merged_radio_button_groups.has (other)
other_first_radio_button_now_selected: not old other.has_selected_radio_button and old other.has_radio_button implies other.first_radio_button_selected
original_radio_button_still_selected: old has_selected_radio_button implies has_selected_radio_button
other_first_radio_button_now_selected: not old has_selected_radio_button and old other.has_radio_button and old merged_radio_button_groups.count = 1 and has_radio_button implies first_radio_button_selected
other_original_radio_button_still_selected: old other.has_selected_radio_button implies other.has_selected_radio_button
feature
crop
world_borderautoscroll_border
cut
extend (v: like item)
`v'
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_containable: may_contain (v)
ensure EV_CONTAINER
has_v: has (v)
fill (other: CONTAINER [EV_WIDGET])
`other'
`other'
COLLECTION
require COLLECTION
other_not_void: other /= Void
extendible: extendible
fit_to_screen
put (v: like item)
item`v'
EV_CONTAINERreplace
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_containable: may_contain (v)
ensure EV_CONTAINER
has_v: has (v)
not_has_old_item: not has (old item)
remove_help_context
`EV_APPLICATION.help_key'
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
help_context_not_void: help_context /= Void
ensure EV_HELP_CONTEXTABLE
no_help_context: help_context = Void
remove_background_pixmap
`Current'
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
pixmap_removed: background_pixmap = Void
replace (v: like item)
item`v'
EV_CONTAINERput
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_containable: may_contain (v)
ensure EV_CONTAINER
has_v: has (v)
not_has_old_item: not has (old item)
set_autoscroll_border (a_border: like autoscroll_border)
autoscroll_border`a_border'
require
a_border_positive: a_border >= 0
ensure
set: autoscroll_border = a_border
set_background_color (a_color: like background_color)
`a_color'background_color
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure EV_COLORIZABLE
background_color_assigned: background_color.is_equal (a_color)
set_data (some_data: like data)
`some_data'data
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
set_foreground_color (a_color: like foreground_color)
`a_color'foreground_color
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= Void
ensure EV_COLORIZABLE
foreground_color_assigned: foreground_color.is_equal (a_color)
set_help_context (an_help_context: like help_context)
`an_help_context'help_context
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
an_help_context_not_void: an_help_context /= Void
ensure EV_HELP_CONTEXTABLE
help_context_assigned: help_context.is_equal (an_help_context)
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
set_minimum_size (a_minimum_width, a_minimum_height: INTEGER_32)
`a_minimum_height'minimum_height
`a_minimum_width'minimum_width
widthheight
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width >= 0
a_minimum_height_positive: a_minimum_height >= 0
ensure EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width
minimum_height_assigned: minimum_height = a_minimum_height
minimum_height_set_by_user_set: minimum_height_set_by_user
minimum_width_set_by_user_set: minimum_width_set_by_user
set_minimum_width (a_minimum_width: INTEGER_32)
`a_minimum_width'minimum_width
width`a_minimum_width'
minimum_width
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width >= 0
ensure EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width
minimum_width_set_by_user_set: minimum_width_set_by_user
set_background_pixmap (a_pixmap: EV_PIXMAP)
`a_pixmap'`Current'
`pixmap'`a_pixmap'
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
pixmap_not_void: a_pixmap /= Void
set_pointer_style (a_cursor: like pointer_style)
`a_cursor'pointer_style
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
a_cursor_not_void: a_cursor /= Void
ensure EV_WIDGET
pointer_style_assigned: pointer_style.is_equal (a_cursor)
set_scroll_speed (a_scroll_speed: like scroll_speed)
scroll_speed`a_scroll_speed'
require
a_scroll_speed_positive: a_scroll_speed >= 0.0
ensure
set: scroll_speed = a_scroll_speed
set_world (a_world: like world)
world`a_world'
require
a_world_not_void: a_world /= Void
ensure
set: world = a_world
set_world_border (a_border: like world_border)
world_border`a_border'
require
a_border_positive: a_border >= 0
ensure
set: world_border = a_border
feature
frozen free_id
object_id
IDENTIFIED
ensure IDENTIFIED
object_freed: id_freed
prune (v: EV_WIDGET)
`v'
EV_CELL
require COLLECTION
prunable: prunable
ensure then EV_CELL
not has (v)
prune_all (v: EV_WIDGET)
`v'
object_comparison
COLLECTION
require COLLECTION
prunable: prunable
ensure COLLECTION
no_more_occurrences: not has (v)
wipe_out
item
EV_CELL
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: is_empty
feature
linear_representation: LINEAR [like item]
EV_CELL
feature
copy (other: like Current)
`other'
EV_ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: like Current)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: like Current
ANY
ensure ANY
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: like Current
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
propagate_background_color
background_color
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
background_color_propagated: background_color_propagated
propagate_foreground_color
foreground_color
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
ensure EV_CONTAINER
foreground_color_propagated: foreground_color_propagated
refresh_now
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
feature
destroy
`Current'
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
`a_widget'parentparentparent
EV_CONTAINER
require EV_CONTAINER
not_destroyed: not is_destroyed
may_contain (v: EV_WIDGET): BOOLEAN
`v'`Current'
EV_CONTAINER
parent_of_source_allows_docking: BOOLEAN
real_source
EV_DOCKABLE_SOURCE
source_has_current_recursive (source: EV_DOCKABLE_SOURCE): BOOLEAN
`source'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
source_not_void: source /= Void
feature
conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
dock_ended_actions: EV_NOTIFY_ACTION_SEQUENCE
`Current'
EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
ensure EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
not_void: Result /= Void
dock_started_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
ensure EV_DOCKABLE_SOURCE_ACTION_SEQUENCES
not_void: Result /= Void
docked_actions: EV_DOCKABLE_SOURCE_ACTION_SEQUENCE
EV_DOCKABLE_TARGET_ACTION_SEQUENCES
ensure EV_DOCKABLE_TARGET_ACTION_SEQUENCES
not_void: Result /= Void
drop_actions: EV_PND_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
focus_in_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
focus_out_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_press_actions: EV_KEY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
key_release_actions: EV_KEY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
mouse_wheel_actions: EV_INTEGER_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pick_actions: EV_PND_START_ACTION_SEQUENCE
pebble
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE
`Current'
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= Void
pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
EV_WIDGET_ACTION_SEQUENCES
ensure EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= Void
feature
height: INTEGER_32
minimum_height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.height
minimum_height: INTEGER_32
height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_height
positive_or_zero: Result >= 0
minimum_width: INTEGER_32
width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_width
positive_or_zero: Result >= 0
width: INTEGER_32
minimum_width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.width
x_position: INTEGER_32
x_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.x_position
y_position: INTEGER_32
y_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.y_position
feature
io: STD_FILES
ANY
out: STRING_8
ANYtagged_out
ANY
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
feature
is_destroyed: BOOLEAN
`Current'
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
scroll_speed_positive: scroll_speed >= 0.0
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 EV_MODEL_WORLD_CELL