indexing
description: "[Multi-column lists that allow in-place editing of list row items. By default ALLcolumns are editable. Only one single column item is editable at any time and the widget typewhich can be edited must conform to EV_TEXTABLE."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "6/17/02"
revision: "1.0"
class interface
EV_EDITABLE_LIST
create
make (a_window: EV_WINDOW)
require
window_not_void: a_window /= Void
feature
make (a_window: EV_WINDOW)
require
window_not_void: a_window /= Void
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
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)
column_count: INTEGER_32
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.column_count
cursor: EV_DYNAMIC_LIST_CURSOR [EV_MULTI_COLUMN_LIST_ROW]
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_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
first: like item
CHAIN
require CHAIN
not_empty: not is_empty
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: like item): BOOLEAN
`v'
object_comparison
CHAIN
require CONTAINER
True
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
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
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
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_MULTI_COLUMN_LIST_ROW
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)
last: like item
CHAIN
require CHAIN
not_empty: not is_empty
frozen object_id: INTEGER_32
IDENTIFIED
ensure IDENTIFIED
valid_id: 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_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
pixmaps_height: INTEGER_32
EV_ITEM_PIXMAP_SCALER
require EV_ITEM_PIXMAP_SCALER
not_destroyed: not is_destroyed
ensure EV_ITEM_PIXMAP_SCALER
bridge_ok: Result = implementation.pixmaps_height
pixmaps_width: INTEGER_32
EV_ITEM_PIXMAP_SCALER
require EV_ITEM_PIXMAP_SCALER
not_destroyed: not is_destroyed
ensure EV_ITEM_PIXMAP_SCALER
bridge_ok: Result = implementation.pixmaps_width
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
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
retrieve_item_by_data (some_data: ANY; should_compare_objects: BOOLEAN): EV_MULTI_COLUMN_LIST_ROW
`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_items_by_data (some_data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_MULTI_COLUMN_LIST_ROW]
`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
row_height: INTEGER_32
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.row_height
selected_item: like item
selected_items
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.selected_item
selected_items: DYNAMIC_LIST [like item]
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: lists_equal (Result, implementation.selected_items)
target_name: STRING_GENERAL
`Current'
EV_ABSTRACT_PICK_AND_DROPABLE
tooltip: STRING_32
`Current'
`Result'
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
bridge_ok: equal (Result, implementation.tooltip)
not_void: Result /= Void
cloned: Result /= implementation.tooltip
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
index_set: INTEGER_INTERVAL
CHAIN
require INDEXABLE
True
ensure INDEXABLE
not_void: Result /= Void
ensure then CHAIN
count_definition: Result.count = count
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_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'
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: 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
after: BOOLEAN
LIST
require LINEAR
True
all_columns_editable: BOOLEAN
all_rows_editable: BOOLEAN
before: BOOLEAN
LIST
require BILINEAR
True
column_alignment (a_column: INTEGER_32): EV_TEXT_ALIGNMENT
`Result'`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column >= 1 and a_column <= column_count
ensure EV_MULTI_COLUMN_LIST
result_not_void: Result /= Void
bridge_ok: Result.is_equal (implementation.column_alignment (a_column))
column_editable (i: INTEGER_32): BOOLEAN
column_title (a_column: INTEGER_32): STRING_32
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_positive: a_column >= 1
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result.is_equal (implementation.column_title (a_column))
cloned: Result /= implementation.column_title (a_column)
column_width (a_column: INTEGER_32): INTEGER_32
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column >= 1 and a_column <= column_count
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.column_width (a_column)
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_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
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
FINITE
require CONTAINER
True
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_MULTI_COLUMN_LIST_ROW): BOOLEAN
`v'
`has (v)'
COLLECTION
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
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_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
multiple_selection_enabled: BOOLEAN
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.multiple_selection_enabled
object_comparison: BOOLEAN
equal`='
`='
CONTAINER
off: BOOLEAN
CHAIN
require TRAVERSABLE
True
prunable: BOOLEAN
DYNAMIC_CHAIN
require COLLECTION
True
readable: BOOLEAN
SEQUENCE
require ACTIVE
True
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
row_editable (i: INTEGER_32): BOOLEAN
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))
set_pixmaps_size (a_width: INTEGER_32; a_height: INTEGER_32)
`Current'
EV_ITEM_PIXMAP_SCALER
require EV_ITEM_PIXMAP_SCALER
not_destroyed: not is_destroyed
valid_width: a_width > 0
valid_height: a_height > 0
ensure EV_ITEM_PIXMAP_SCALER
width_set: pixmaps_width = a_width
height_set: pixmaps_height = a_height
title_shown: BOOLEAN
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
bridge_ok: Result = implementation.title_shown
valid_cursor (p: CURSOR): BOOLEAN
`p'
`p'
`Current'
EV_DYNAMIC_LIST
require CURSOR_STRUCTURE
True
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.valid_cursor (p)
valid_cursor_index (i: INTEGER_32): BOOLEAN
`i'
CHAIN
ensure CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))
valid_index (i: INTEGER_32): BOOLEAN
`i'
CHAIN
require TABLE
True
ensure then INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
ensure then CHAIN
valid_index_definition: Result = ((i >= 1) and (i <= count))
writable: BOOLEAN
SEQUENCE
require ACTIVE
True
feature
align_text_center (a_column: INTEGER_32)
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 1 and a_column <= column_count
ensure EV_MULTI_COLUMN_LIST
center_aligned: column_alignment (a_column).is_center_aligned
align_text_left (a_column: INTEGER_32)
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 1 and a_column <= column_count
ensure EV_MULTI_COLUMN_LIST
left_aligned: column_alignment (a_column).is_left_aligned
align_text_right (a_column: INTEGER_32)
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 1 and a_column <= column_count
ensure EV_MULTI_COLUMN_LIST
right_aligned: column_alignment (a_column).is_right_aligned
center_pointer
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
compare_objects
equal
`='
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
object_comparison
compare_references
`='
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
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_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_multiple_selection
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
not_multiple_selection_enabled: not multiple_selection_enabled
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_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_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_multiple_selection
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
multiple_selection_enabled: multiple_selection_enabled
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_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
ensure_item_visible (an_item: EV_MULTI_COLUMN_LIST_ROW)
`an_item'`Current'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
is_displayed: is_displayed
an_item_contained: has (an_item)
hide
`Current'
is_show_requested`False'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
hide_title_row
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
not_title_shown: not title_shown
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
remove_selection
selected_items
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
selected_items_empty: selected_items.is_empty
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)
show
`Current'
`True'
is_show_requested`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
show_title_row
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
ensure EV_MULTI_COLUMN_LIST
title_shown: title_shown
feature
back
EV_DYNAMIC_LIST
require BILINEAR
not_before: not before
finish
CHAIN
require LINEAR
True
ensure then CHAIN
at_last: not is_empty implies islast
forth
EV_DYNAMIC_LIST
require LINEAR
not_after: not after
ensure then LIST
moved_forth: index = old index + 1
go_i_th (i: INTEGER_32)
`i'
EV_DYNAMIC_LIST
require CHAIN
valid_cursor_index: valid_cursor_index (i)
ensure CHAIN
position_expected: index = i
go_to (p: CURSOR)
`p'
EV_DYNAMIC_LIST
require CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER_32)
`i'
EV_DYNAMIC_LIST
ensure CHAIN
too_far_right: (old index + i > count) implies exhausted
too_far_left: (old index + i < 1) implies exhausted
expected_index: (not exhausted) implies (index = old index + i)
search (v: like item)
item`v'
`v'
exhausted
object_comparison
BILINEAR
ensure LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, item)
item_found: (not exhausted and not object_comparison) implies v = item
start
EV_DYNAMIC_LIST
require TRAVERSABLE
True
ensure then CHAIN
at_first: not is_empty implies isfirst
ensure then EV_DYNAMIC_LIST
empty_implies_after: is_empty implies after
feature
append (s: SEQUENCE [like item])
`s'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
sequence_not_void: s /= Void
sequence_not_current: s /= Current
not_parented: not s.there_exists (agent (v: like item): BOOLEAN
)
ensure EV_DYNAMIC_LIST
count_increased: old count + s.count = count
cursor_not_moved: (index = old index) or (after and old after)
fill (other: CONTAINER [EV_MULTI_COLUMN_LIST_ROW])
`other'
`other'
CHAIN
require COLLECTION
other_not_void: other /= Void
extendible: extendible
force (v: like item)
`v'
EV_DYNAMIC_LISTextend
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_is_last: v = last
count_increased: count = old count + 1
cursor_not_moved: (index = old index) or (after and old after)
dl_force (v: like item)
`v'
SEQUENCE
require SEQUENCE
extendible: extendible
ensure then SEQUENCE
new_count: count = old count + 1
item_inserted: has (v)
merge_left (other: like Current)
`other'
`other'
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_before: not before
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: count = old count + old other.count
new_index: index = old index + old other.count
other_is_empty: other.is_empty
merge_right (other: like Current)
`other'
`other'
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_after: not after
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: count = old count + old other.count
same_index: index = old index
other_is_empty: other.is_empty
put (v: like item)
`v'
replace
CHAIN
require COLLECTION
extendible: extendible
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then SET
in_set_already: old has (v) implies (count = old count)
added_to_set: not old has (v) implies (count = old count + 1)
ensure then CHAIN
same_count: count = old count
put_front (v: like item)
`v'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_is_first: v = first
count_increased: count = old count + 1
cursor_not_moved: (index = old index + 1) or (before and old before)
put_i_th (v: like item; i: INTEGER_32)
`i'`v'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
valid_index: i > 0 and i <= count
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
item_replaced: v = i_th (i)
not_has_old_item: not has (old i_th (i))
old_item_parent_void: (old i_th (i)).parent = Void
count_same: count = old count
cursor_not_moved: index = old index
put_left (v: like item)
`v'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
not_before: not before
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_at_index_plus_one: v = i_th (index - 1)
count_increased: count = old count + 1
cursor_not_moved: index = old index + 1
put_right (v: like item)
`v'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
not_after: not after
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_at_index_plus_one: v = i_th (index + 1)
count_increased: count = old count + 1
cursor_not_moved: index = old index
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_tooltip
tooltip
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
tooltip_removed: tooltip.is_empty
replace (v: like item)
`v'
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
item_replaced: v = item
not_has_old_item: not has (old item)
old_item_parent_void: (old item).parent = Void
count_same: count = old count
cursor_not_moved: index = old index
resize_column_to_content (a_column: INTEGER_32)
`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 0 and a_column <= column_count
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_column_alignment (an_alignment: EV_TEXT_ALIGNMENT; a_column: INTEGER_32)
`a_column'`an_alignment'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 1 and a_column <= column_count
alignment_not_void: an_alignment /= Void
ensure EV_MULTI_COLUMN_LIST
column_alignment_assigned: column_alignment (a_column).is_equal (an_alignment)
set_column_alignments (alignments: LINKED_LIST [EV_TEXT_ALIGNMENT])
`alignments'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
alignments_not_void: alignments /= Void
ensure EV_MULTI_COLUMN_LIST
column_alignments_assigned: column_alignments_assigned (alignments)
set_column_title (a_title: STRING_GENERAL; a_column: INTEGER_32)
`a_title'column_title`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_positive: a_column > 0
a_title_not_void: a_title /= Void
ensure EV_MULTI_COLUMN_LIST
a_title_assigned: column_title (a_column).is_equal (a_title)
column_count_valid: column_count >= a_column
cloned: column_title (a_column) /= a_title
set_column_titles (titles: ARRAY [STRING_GENERAL])
`titles'
`Current'
column_count
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
titles_not_void: titles /= Void
ensure EV_MULTI_COLUMN_LIST
column_count_valid: column_count >= titles.count
column_titles_assigned: column_titles_assigned (titles)
set_column_width (a_width: INTEGER_32; a_column: INTEGER_32)
`a_width'column_width`a_column'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
a_column_within_range: a_column > 0
a_width_positive: a_width >= 0
ensure EV_MULTI_COLUMN_LIST
column_count_valid: column_count >= a_column
a_width_assigned: a_width = column_width (a_column)
set_column_widths (widths: ARRAY [INTEGER_32])
`widths'
EV_MULTI_COLUMN_LIST
require EV_MULTI_COLUMN_LIST
not_destroyed: not is_destroyed
widths_not_void: widths /= Void
ensure EV_MULTI_COLUMN_LIST
column_count_valid: column_count >= widths.count
column_widths_assigned: column_widths_assigned (widths)
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_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_tooltip (a_tooltip: STRING_GENERAL)
`a_tooltip'tooltip
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
tooltip: a_tooltip /= Void
ensure EV_TOOLTIPABLE
tooltip_assigned: tooltip.is_equal (a_tooltip)
cloned: tooltip /= a_tooltip
swap (i: INTEGER_32)
`i'
EV_DYNAMIC_LIST
require CHAIN
not_off: not off
valid_index: valid_index (i)
ensure CHAIN
swapped_to_item: item = old i_th (i)
swapped_from_item: i_th (i) = old item
feature
prune (v: like item)
`v'
`v'
EV_DYNAMIC_LIST
require COLLECTION
prunable: prunable
ensure then SET
removed_count_change: old has (v) implies (count = old count - 1)
not_removed_no_count_change: not old has (v) implies (count = old count)
item_deleted: not has (v)
ensure then EV_DYNAMIC_LIST
not_has_v: not has (v)
had_item_implies_parent_void: old has (v) implies v.parent = Void
had_item_implies_count_decreased: old has (v) implies count = old count - 1
had_item_and_was_after_implies_index_decreased: (old after and old has (v)) implies index = old index - 1
prune_all (v: like item)
`v'
object_comparison
exhausted
DYNAMIC_CHAIN
require COLLECTION
prunable: prunable
ensure COLLECTION
no_more_occurrences: not has (v)
ensure then DYNAMIC_CHAIN
is_exhausted: exhausted
remove
after
EV_DYNAMIC_LIST
require ACTIVE
prunable: prunable
writable: writable
ensure then DYNAMIC_LIST
after_when_empty: is_empty implies after
ensure then EV_DYNAMIC_LIST
v_removed: not has (old item)
parent_void: (old item).parent = Void
count_decreased: count = old count - 1
index_same: index = old index
remove_left
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
left_exists: index > 1
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
new_index: index = old index - 1
ensure then EV_DYNAMIC_LIST
left_neighbor_removed: not has (old i_th (index - 1))
parent_void: (old i_th (index - 1)).parent = Void
index_decreased: index = old index - 1
remove_right
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
right_exists: index < count
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
same_index: index = old index
ensure then EV_DYNAMIC_LIST
right_neighbor_removed: not has (old i_th (index + 1))
parent_void: (old i_th (index + 1)).parent = Void
index_same: index = old index
remove_selected_item
wipe_out
EV_DYNAMIC_LIST
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: is_empty
ensure then DYNAMIC_LIST
is_before: before
feature
linear_representation: LINEAR [EV_MULTI_COLUMN_LIST_ROW]
LINEAR
require CONTAINER
True
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
refresh_now
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
feature
changeable_comparison_criterion: BOOLEAN is False
object_comparison
EV_ITEM_LIST
feature
end_edit_actions: ACTION_SEQUENCE [TUPLE]
feature
destroy
`Current'
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
is_parent_recursive (a_row: EV_MULTI_COLUMN_LIST_ROW): BOOLEAN
`a_row'`Current'
EV_MULTI_COLUMN_LIST
require EV_DYNAMIC_LIST
a_list_not_void: a_row /= Void
not_destroyed: not is_destroyed
parent_of_source_allows_docking: BOOLEAN
real_source
EV_DOCKABLE_SOURCE
same (other: EV_ANY): BOOLEAN
`other'`Current'
EV_DYNAMIC_LIST
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
edit_row (x, y, button: INTEGER_32; x_tilt, y_tilt, pressure: REAL_64; a_screen_x, a_screen_y: INTEGER_32)
feature
extend (v: like item)
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= Void
v_parent_void: v.parent = Void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_is_last: v = last
count_increased: count = old count + 1
cursor_not_moved: (index = old index) or (after and old after)
feature
column_resized_actions: EV_COLUMN_ACTION_SEQUENCE
EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
ensure EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
not_void: Result /= Void
column_title_click_actions: EV_COLUMN_ACTION_SEQUENCE
EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
ensure EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
not_void: Result /= Void
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
deselect_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE
EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
ensure EV_MULTI_COLUMN_LIST_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
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
select_actions: EV_MULTI_COLUMN_LIST_ROW_SELECT_ACTION_SEQUENCE
EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
ensure EV_MULTI_COLUMN_LIST_ACTION_SEQUENCES
not_void: Result /= Void
feature
do_all (action: PROCEDURE [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW]])
`action'
`action'
LINEAR
require TRAVERSABLE
action_exists: action /= Void
do_if (action: PROCEDURE [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW]]; test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN])
`action'`test'
`action'`test'
LINEAR
require TRAVERSABLE
action_exists: action /= Void
test_exits: test /= Void
for_all (test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: test /= Void
ensure then LINEAR
empty: is_empty implies Result
there_exists (test: FUNCTION [ANY, TUPLE [EV_MULTI_COLUMN_LIST_ROW], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: test /= 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
select_item (a_string: STRING_GENERAL; i: INTEGER_32)
feature
is_destroyed: BOOLEAN
`Current'
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
feature
change_widget_type (i: INTEGER_32; a_widget: EV_TEXTABLE)
require
editable_column: column_editable (i)
set_all_columns_editable
require
has_columns: column_count > 0
set_all_rows_editable
set_column_editable (a_flag: BOOLEAN; i: INTEGER_32)
set_non_empty_column_values (a_flag: BOOLEAN)
set_row_editable (a_flag: BOOLEAN; i: INTEGER_32)
set_unique_column_values (a_flag: BOOLEAN)
set_with_previous_text
`saved text'
invariant
has_relative_window: relative_window /= Void
change_widgets_not_void: change_widgets /= Void
editable_columns_not_void: editable_columns /= Void
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
EV_ITEM_LIST
parent_of_items_is_current: is_usable and then not is_empty implies parent_of_items_is_current
items_unique: is_usable and not is_empty implies items_unique
LIST
before_definition: before = (index = 0)
after_definition: after = (index = count + 1)
CHAIN
non_negative_index: index >= 0
index_small_enough: index <= count + 1
off_definition: off = ((index = 0) or (index = count + 1))
isfirst_definition: isfirst = ((not is_empty) and (index = 1))
islast_definition: islast = ((not is_empty) and (index = count))
item_corresponds_to_index: (not off) implies (item = i_th (index))
index_set_has_same_count: index_set.count = count
ACTIVE
writable_constraint: writable implies readable
empty_constraint: is_empty implies (not readable) and (not writable)
INDEXABLE
index_set_not_void: index_set /= Void
BILINEAR
not_both: not (after and before)
before_constraint: before implies off
LINEAR
after_constraint: after implies off
TRAVERSABLE
empty_constraint: is_empty implies off
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
DYNAMIC_CHAIN
extendible: extendible
EV_ITEM_PIXMAP_SCALER
pixmaps_size_positive: pixmaps_height > 0 and pixmaps_width > 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_EDITABLE_LIST