indexing
description: "List of items which can be selected by the user."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_MENU
create
make
make_by_id (id: INTEGER)
id
WEL_RESOURCE
require WEL_RESOURCE
valid_id: id > 0
ensure WEL_RESOURCE
not_shared: not shared
make_by_name (name: STRING)
name
WEL_RESOURCE
require WEL_RESOURCE
name_not_void: name /= void
name_not_empty: not name.is_empty
ensure WEL_RESOURCE
not_shared: not shared
make_by_pointer (a_pointer: POINTER)
itema_pointer
item
a_pointer
WEL_ANY
ensure WEL_ANY
item_set: item = a_pointer
shared: shared
make_track
feature
item: POINTER
WEL_ANY
popup_menu (position: INTEGER): WEL_MENU
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
popup_exists: popup_exists (position)
ensure
result_not_void: Result /= void
feature
count: INTEGER
require
exists: exists
ensure
positive_result: Result >= 0
feature
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
id_string (an_id: INTEGER): STRING
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
result_not_void: Result /= void
item_checked (an_id: INTEGER): BOOLEAN
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
item_enabled (an_id: INTEGER): BOOLEAN
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
item_exists (an_id: INTEGER): BOOLEAN
an_id
require
exists: exists
positive_id: an_id > 0
popup_exists (position: INTEGER): BOOLEAN
require
exists: exists
positive_position: position >= 0
position_enabled (position: INTEGER): BOOLEAN
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
check_item (an_id: INTEGER)
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
item_checked: item_checked (an_id)
disable_item (an_id: INTEGER)
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
item_disabled: not item_enabled (an_id)
disable_position (position: INTEGER)
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
ensure
position_disabled: not position_enabled (position)
enable_item (an_id: INTEGER)
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
item_enabled: item_enabled (an_id)
enable_position (position: INTEGER)
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
ensure
position_enabled: position_enabled (position)
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
uncheck_item (an_id: INTEGER)
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
item_unchecked: not item_checked (an_id)
feature
append_bitmap (bitmap: WEL_BITMAP; an_id: INTEGER)
bitmapan_id
require
exists: exists
bitmap_not_void: bitmap /= void
bitmap_exists: bitmap.exists
positive_id: an_id > 0
item_not_exists: not item_exists (an_id)
ensure
new_count: count = old count + 1
item_exists: item_exists (an_id)
append_popup (a_menu: WEL_MENU; a_title: STRING)
a_menua_title
require
exists: exists
a_menu_not_void: a_menu /= void
a_menu_exists: a_menu.exists
a_title_not_void: a_title /= void
ensure
new_count: count = old count + 1
append_separator
require
exists: exists
ensure
new_count: count = old count + 1
append_string (a_string: STRING; an_id: INTEGER)
a_stringan_id
require
exists: exists
a_string_not_void: a_string /= void
positive_id: an_id > 0
item_not_exists: not item_exists (an_id)
ensure
new_count: count = old count + 1
item_exists: item_exists (an_id)
string_set: id_string (an_id).is_equal (a_string)
append_string_with_break (a_string: STRING; an_id: INTEGER; has_separator: BOOLEAN)
has_separator
require
exists: exists
a_string_not_void: a_string /= void
positive_id: an_id > 0
item_not_exists: not item_exists (an_id)
ensure
new_count: count = old count + 1
item_exists: item_exists (an_id)
string_set: id_string (an_id).is_equal (a_string)
insert_bitmap (bitmap: WEL_BITMAP; a_position, an_id: INTEGER)
bitmapa_position
an_id
require
exists: exists
a_position_large_enough: a_position >= 0
a_position_small_enough: a_position <= count
bitmap_not_void: bitmap /= void
bitmap_exists: bitmap.exists
positive_id: an_id > 0
item_not_exists: not item_exists (an_id)
ensure
new_count: count = old count + 1
insert_popup (a_menu: WEL_MENU; a_position: INTEGER; a_title: STRING)
a_menua_position
a_title
require
exists: exists
a_menu_not_void: a_menu /= void
a_menu_exists: a_menu.exists
a_title_not_void: a_title /= void
a_position_large_enough: a_position >= 0
a_position_small_enough: a_position <= count
ensure
new_count: count = old count + 1
popup_menu_set: popup_menu (a_position).item = a_menu.item
insert_separator (a_position: INTEGER)
a_position
require
exists: exists
a_position_large_enough: a_position >= 0
a_position_small_enough: a_position <= count
ensure
new_count: count = old count + 1
insert_string (a_string: STRING; a_position, an_id: INTEGER)
a_stringa_position
an_id
require
exists: exists
a_position_large_enough: a_position >= 0
a_position_small_enough: a_position <= count
a_string_not_void: a_string /= void
positive_id: an_id > 0
item_not_exists: not item_exists (an_id)
ensure
new_count: count = old count + 1
string_set: id_string (an_id).is_equal (a_string)
modify_string (a_string: STRING; an_id: INTEGER)
an_id
a_string
require
exists: exists
a_string_not_void: a_string /= void
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
string_set: id_string (an_id).is_equal (a_string)
set_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
feature
delete_item (an_id: INTEGER)
an_id
require
exists: exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
ensure
new_count: count = old count - 1
item_not_exists: not item_exists (an_id)
delete_position (position: INTEGER)
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
ensure
new_count: count = old count - 1
dispose
Current
Current
WEL_ANY
remove_position (position: INTEGER)
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
ensure
new_count: count = old count - 1
feature
position_to_item_id (position: INTEGER): INTEGER
position
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position < count
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
hilite_menu_item (window: WEL_COMPOSITE_WINDOW; an_id: INTEGER)
an_id
window
require
exists: exists
window_not_void: window /= void
window_exists: window.exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
show_track (x, y: INTEGER; window: WEL_COMPOSITE_WINDOW)
xy
window
on_menu_command
require
exists: exists
not_empty: count > 0
window_not_void: window /= void
window_exists: window.exists
show_track_with_option (x, y: INTEGER; window: WEL_COMPOSITE_WINDOW; option: INTEGER; rect: WEL_RECT)
option
xy
window
on_menu_command
rect
require
exists: exists
not_empty: count > 0
window_not_void: window /= void
window_exists: window.exists
unhilite_menu_item (window: WEL_COMPOSITE_WINDOW; an_id: INTEGER)
an_id
window
require
exists: exists
window_not_void: window /= void
window_exists: window.exists
positive_id: an_id > 0
item_exists: item_exists (an_id)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_MENU