indexing
description: "Base class for all items that may be held in EV_ITEM_LISTs."
status: "See notice at end of class."
keywords: "item"
date: "$Date$"
revision: "$Revision$"
deferred class interface
EV_ITEM
feature
frozen default_create
EV_ANY
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
accept_cursor: EV_CURSOR
Result
pebble
EV_PICK_AND_DROPABLE
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor
data: ANY
EV_ANY
deny_cursor: EV_CURSOR
Result
pebble
EV_PICK_AND_DROPABLE
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor
frozen id_object (an_id: INTEGER): IDENTIFIED
an_id
IDENTIFIED
ensure IDENTIFIED
consistent: Result = void or else Result.object_id = an_id
frozen object_id: INTEGER
IDENTIFIED
ensure IDENTIFIED
valid_id: id_object (Result) = Current
parent: EV_ITEM_LIST [EV_ITEM]
Current
require EV_CONTAINABLE
not_destroyed: not is_destroyed
ensure then
bridge_ok: Result = implementation.parent
pebble: ANY
EV_PICK_AND_DROPABLE
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble
pebble_function: FUNCTION [ANY, TUPLE, ANY]
EV_PICK_AND_DROPABLE
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
Current
EV_PICK_AND_DROPABLE
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position
pebble_y_position: INTEGER
Current
EV_PICK_AND_DROPABLE
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_y_position
pixmap: EV_PIXMAP
Current
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
bridge_ok: (Result = void and implementation.pixmap = void) or Result.is_equal (implementation.pixmap)
target_name: STRING
Current
EV_ABSTRACT_PICK_AND_DROPABLE
feature
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
feature
disable_pebble_positioning
Falsepebble_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
enable_pebble_positioning
Truepebble_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
remove_pebble
pebbleVoidpebble_function
EV_PICK_AND_DROPABLE
ensure EV_ABSTRACT_PICK_AND_DROPABLE
pebble_removed: pebble = void and pebble_function = void
set_accept_cursor (a_cursor: EV_CURSOR)
a_cursor
pebble
EV_PICK_AND_DROPABLE
ensure EV_ABSTRACT_PICK_AND_DROPABLE
accept_cursor_assigned: accept_cursor.is_equal (a_cursor)
set_deny_cursor (a_cursor: EV_CURSOR)
a_cursor
EV_PICK_AND_DROPABLE
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_pebble (a_pebble: like pebble)
a_pebblepebble
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_functionpebble
pebble
a_function
FUNCTIONANYTUPLEINTEGERINTEGERANY
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)
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_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)
a_nametarget_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)
feature
remove_pixmap
pixmapVoid
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
ensure EV_PIXMAPABLE
pixmap_removed: pixmap = void
set_data (some_data: like data)
some_datadata
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
set_pixmap (a_pixmap: EV_PIXMAP)
a_pixmappixmap
EV_PIXMAPABLE
require EV_PIXMAPABLE
not_destroyed: not is_destroyed
pixmap_not_void: a_pixmap /= void
ensure EV_PIXMAPABLE
pixmap_assigned: a_pixmap.is_equal (pixmap) and pixmap /= a_pixmap
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)
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void
drop_actions: EV_PND_ACTION_SEQUENCE
EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
ensure EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void
pick_actions: EV_PND_START_ACTION_SEQUENCE
pebble
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_ITEM_ACTION_SEQUENCES
ensure EV_ITEM_ACTION_SEQUENCES
not_void: Result /= void
pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
EV_ITEM_ACTION_SEQUENCES
ensure EV_ITEM_ACTION_SEQUENCES
not_void: Result /= void
pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE
EV_ITEM_ACTION_SEQUENCES
ensure EV_ITEM_ACTION_SEQUENCES
not_void: Result /= void
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (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
end -- EV_ITEM