indexing
description: "[
Node for use with EV_TREE.
]"
legal: "See notice at end of class."
status: "See notice at end of class."
keywords: "tree, item, leaf, node, branch"
date: "$Date$"
revision: "$Revision$"
deferred class interface
EV_TREE_NODE
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
configurable_target_menu_handler: PROCEDURE [ANY, TUPLE [menu: EV_MENU; target_list: ARRAYED_LIST [EV_PND_TARGET_DATA]; source: EV_PICK_AND_DROPABLE; source_pebble: ANY]]
`Current'
EV_PICK_AND_DROPABLE
cursor: EV_DYNAMIC_LIST_CURSOR [EV_TREE_NODE]
EV_DYNAMIC_LIST
require CURSOR_STRUCTURE
True
ensure CURSOR_STRUCTURE
cursor_not_void: Result /= Void
ensure then EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.cursor)
data: ANY
EV_ANY
default_identifier_name: STRING_8
identifier_name
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_not_empty: not Result.is_empty
no_period_in_result: not Result.has ('.')
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
first: like item
CHAIN
require CHAIN
not_empty: not is_empty
full_identifier_path: STRING_8
EV_IDENTIFIABLE
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_correct: parent = Void implies Result.is_equal (identifier_name)
result_correct: parent /= Void implies Result.is_equal (parent.full_identifier_path + "." + identifier_name)
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
has (v: like item): BOOLEAN
`v'
object_comparison
CHAIN
require CONTAINER
True
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
has_recursively (an_item: EV_TREE_NODE): BOOLEAN
`an_item'`Current'
EV_TREE_NODE_LIST
require EV_TREE_NODE_LIST
item_not_void: an_item /= Void
ensure EV_TREE_NODE_LIST
not_found_in_empty: Result implies not is_empty
index_not_changed: old index = index
i_th alias "[]" (i: INTEGER_32): like item
`i'
EV_DYNAMIC_LIST
require TABLE
valid_key: valid_index (i)
ensure then EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.i_th (i))
frozen id_object (an_id: INTEGER_32): ?IDENTIFIED
`an_id'
IDENTIFIED
ensure IDENTIFIED
consistent: Result = Void or else Result.object_id = an_id
identifier_name: STRING_8
default_identifier_name
EV_IDENTIFIABLE
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_not_empty: not Result.is_empty
no_period_in_result: not Result.has ('.')
default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name)
index: INTEGER_32
EV_DYNAMIC_LIST
require LINEAR
True
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.index
index_of (v: like item; i: INTEGER_32): INTEGER_32
`i'`v'
EV_DYNAMIC_LIST
require LINEAR
positive_occurrences: i > 0
ensure LINEAR
non_negative_result: Result >= 0
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.index_of (v, i)
item: EV_TREE_NODE
EV_DYNAMIC_LIST
require TRAVERSABLE
not_off: not off
require ACTIVE
readable: readable
ensure then EV_DYNAMIC_LIST
not_void: Result /= Void
bridge_ok: Result.is_equal (implementation.item)
item_for_iteration: EV_TREE_NODE
LINEAR
require LINEAR
not_off: not off
last: like item
CHAIN
require CHAIN
not_empty: not is_empty
frozen object_id: INTEGER_32
IDENTIFIED
ensure IDENTIFIED
valid_id: Result > 0 implies id_object (Result) = Current
sequential_occurrences (v: like item): INTEGER_32
`v'
object_comparison
LINEAR
require BAG
True
ensure BAG
non_negative_occurrences: Result >= 0
parent: EV_TREE_NODE_LIST
`Current'
require EV_IDENTIFIABLE
not_destroyed: not is_destroyed
ensure EV_IDENTIFIABLE
correct: has_parent implies Result /= Void
correct: not has_parent implies Result = Void
ensure then EV_ITEM
bridge_ok: Result = implementation.parent
parent_tree: EV_TREE
`Current'
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.parent_tree
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
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)
retrieve_item_by_data (some_data: ANY; should_compare_objects: BOOLEAN): EV_TREE_NODE
`Result'`Current'
`some_data'
`should_compare_objects'
EV_DYNAMIC_LIST
ensure EV_DYNAMIC_LIST
not_found_in_empty: Result /= Void implies not is_empty
index_not_changed: old index = index
retrieve_item_recursively_by_data (some_data: ANY; should_compare_objects: BOOLEAN): EV_TREE_NODE
data
`Result'
`should_compare_objects'
EV_TREE_NODE_LIST
ensure EV_TREE_NODE_LIST
not_found_in_empty: Result /= Void implies not is_empty
index_not_changed: old index = index
retrieve_items_by_data (some_data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_TREE_NODE]
`Result'`Current'
`some_data'
`should_compare_objects'
EV_DYNAMIC_LIST
ensure EV_DYNAMIC_LIST
result_not_void: Result /= Void
not_found_in_empty: not Result.is_empty implies not is_empty
index_not_changed: old index = index
retrieve_items_recursively_by_data (some_data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_TREE_NODE]
`Result'`Current'
`some_data'
`should_compare_objects'
EV_TREE_NODE_LIST
ensure EV_TREE_NODE_LIST
result_not_void: Result /= Void
not_found_in_empty: not Result.is_empty implies not is_empty
index_not_changed: old index = index
target_data_function: FUNCTION [ANY, TUPLE [ANY], EV_PND_TARGET_DATA]
EV_ABSTRACT_PICK_AND_DROPABLE
target_name: STRING_GENERAL
`Current'
EV_ABSTRACT_PICK_AND_DROPABLE
text: STRING_32
EV_TEXTABLE
require EV_TEXTABLE
not_destroyed: not is_destroyed
ensure EV_TEXTABLE
bridge_ok: equal (Result, implementation.text)
not_void: Result /= Void
cloned: Result /= implementation.text
no_carriage_returns: not Result.has ('%R')
tooltip: STRING_32
`Current'
`Result'
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
bridge_ok: is_bridge_ok (Result)
not_void: Result /= Void
cloned: is_cloned (Result)
infix "@" (i: INTEGER_32): like item assign put_i_th
`i'
CHAINi_th
CHAIN
require TABLE
valid_key: valid_index (i)
feature
count: INTEGER_32
EV_DYNAMIC_LIST
require FINITE
True
require SET
True
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.count
height: INTEGER_32
minimum_height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.height
index_set: INTEGER_INTERVAL
CHAIN
require INDEXABLE
True
ensure INDEXABLE
not_void: Result /= Void
ensure then CHAIN
count_definition: Result.count = count
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
occurrences (v: like item): INTEGER_32
`v'
object_comparison
CHAIN
require BAG
True
require LINEAR
True
ensure BAG
non_negative_occurrences: Result >= 0
screen_x: INTEGER_32
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.screen_x
screen_y: INTEGER_32
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.screen_y
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
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 (other /= Void and then 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))
frozen is_deep_equal (other: EV_TREE_NODE): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: EV_TREE_NODE): BOOLEAN
`other'
LIST
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then LIST
indices_unchanged: index = old index and other.index = old other.index
true_implies_same_size: Result implies count = other.count
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: EV_TREE_NODE): 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
after: BOOLEAN
LIST
require LINEAR
True
before: BOOLEAN
LIST
require BILINEAR
True
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
exhausted: BOOLEAN
LINEAR
ensure LINEAR
exhausted_when_off: off implies Result
extendible: BOOLEAN is True
DYNAMIC_CHAIN
full: BOOLEAN is False
EV_DYNAMIC_LIST
has_identifier_name_set: BOOLEAN
EV_IDENTIFIABLE
has_parent: BOOLEAN
EV_IDENTIFIABLE
is_empty: BOOLEAN
FINITE
require CONTAINER
True
is_expanded: BOOLEAN
`Current'
require
not_destroyed: not is_destroyed
is_inserted (v: EV_TREE_NODE): BOOLEAN
`v'
`has (v)'
COLLECTION
is_selectable: BOOLEAN
enable_select
EV_SELECTABLE
require EV_SELECTABLE
not_destroyed: not is_destroyed
is_selected: BOOLEAN
EV_SELECTABLE
require EV_SELECTABLE
not_destroyed: not is_destroyed
ensure EV_SELECTABLE
bridge_ok: is_selectable implies Result = implementation.is_selected
isfirst: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
islast: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
mode_is_configurable_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_configurable_target_menu
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_