class MENU
All features
Direct parents
non-conformant parents
COLOR_LIST
Summary
creation features
make
exported features
make
open
(x:
INTEGER
, y:
INTEGER
)
add_text_entry
(text:
UNICODE_STRING
, action:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]])
add_entry
(w:
WIDGET
, action:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]])
add_sub_menu_enty
(w:
WIDGET
, menu: MENU)
add_space
elements
:
FAST_ARRAY
[
E_
][
WIDGET
]
actions
:
FAST_ARRAY
[
E_
][
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]]]
activate_proc
:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 1
[
A_
][
INTEGER
]]
list_window
:
LIST_WINDOW
shared_list_window
:
FAST_ARRAY
[
E_
][
LIST_WINDOW
]
run_action
(i:
INTEGER
)
white_color
:
COLOR
black_color
:
COLOR
dim_grey_color
:
COLOR
dark_grey_color
:
COLOR
grey_color
:
COLOR
light_grey_color
:
COLOR
dark_blue_color
:
COLOR
medium_blue_color
:
COLOR
blue_color
:
COLOR
royal_blue_color
:
COLOR
deep_sky_blue_color
:
COLOR
sky_blue_color
:
COLOR
light_sky_blue_color
:
COLOR
steel_blue_color
:
COLOR
light_steel_blue_color
:
COLOR
light_blue_color
:
COLOR
pale_turquoise_color
:
COLOR
dark_turquoise_color
:
COLOR
medium_turquoise_color
:
COLOR
turquoise_color
:
COLOR
dark_cyan_color
:
COLOR
cyan_color
:
COLOR
light_cyan_color
:
COLOR
dark_green_color
:
COLOR
green_color
:
COLOR
light_green_color
:
COLOR
yellow_green_color
:
COLOR
dark_khaki_color
:
COLOR
khaki_color
:
COLOR
yellow_color
:
COLOR
light_yellow_color
:
COLOR
gold_color
:
COLOR
beige_color
:
COLOR
chocolate_color
:
COLOR
firebrick_color
:
COLOR
brown_color
:
COLOR
dark_salmon_color
:
COLOR
salmon_color
:
COLOR
light_salmon_color
:
COLOR
dark_orange_color
:
COLOR
orange_color
:
COLOR
orange_red_color
:
COLOR
dark_red_color
:
COLOR
red_color
:
COLOR
hot_pink_color
:
COLOR
deep_pink_color
:
COLOR
pink_color
:
COLOR
light_pink_color
:
COLOR
pale_violet_red_color
:
COLOR
maroon_color
:
COLOR
medium_violet_red_color
:
COLOR
violet_red_color
:
COLOR
violet_color
:
COLOR
dark_magenta_color
:
COLOR
magenta_color
:
COLOR
dark_violet_color
:
COLOR
blue_violet_color
:
COLOR
medium_purple_color
:
COLOR
purple_color
:
COLOR
Details
make
make
open
(x:
INTEGER
, y:
INTEGER
)
add_text_entry
(text:
UNICODE_STRING
, action:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]])
require
text /= Void
action /= Void
add_entry
(w:
WIDGET
, action:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]])
require
w /= Void
add_sub_menu_enty
(w:
WIDGET
, menu: MENU)
add_space
elements
:
FAST_ARRAY
[
E_
][
WIDGET
]
actions
:
FAST_ARRAY
[
E_
][
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 2
[
A_
,
B_
][
INTEGER
INTEGER
]]]
activate_proc
:
PROCEDURE
[
O_
->
TUPLE
][
TUPLE 1
[
A_
][
INTEGER
]]
list_window
:
LIST_WINDOW
shared_list_window
:
FAST_ARRAY
[
E_
][
LIST_WINDOW
]
run_action
(i:
INTEGER
)
white_color
:
COLOR
black_color
:
COLOR
dim_grey_color
:
COLOR
dark_grey_color
:
COLOR
grey_color
:
COLOR
light_grey_color
:
COLOR
dark_blue_color
:
COLOR
medium_blue_color
:
COLOR
blue_color
:
COLOR
royal_blue_color
:
COLOR
deep_sky_blue_color
:
COLOR
sky_blue_color
:
COLOR
light_sky_blue_color
:
COLOR
steel_blue_color
:
COLOR
light_steel_blue_color
:
COLOR
light_blue_color
:
COLOR
pale_turquoise_color
:
COLOR
dark_turquoise_color
:
COLOR
medium_turquoise_color
:
COLOR
turquoise_color
:
COLOR
dark_cyan_color
:
COLOR
cyan_color
:
COLOR
light_cyan_color
:
COLOR
dark_green_color
:
COLOR
green_color
:
COLOR
light_green_color
:
COLOR
yellow_green_color
:
COLOR
dark_khaki_color
:
COLOR
khaki_color
:
COLOR
yellow_color
:
COLOR
light_yellow_color
:
COLOR
gold_color
:
COLOR
beige_color
:
COLOR
chocolate_color
:
COLOR
firebrick_color
:
COLOR
brown_color
:
COLOR
dark_salmon_color
:
COLOR
salmon_color
:
COLOR
light_salmon_color
:
COLOR
dark_orange_color
:
COLOR
orange_color
:
COLOR
orange_red_color
:
COLOR
dark_red_color
:
COLOR
red_color
:
COLOR
hot_pink_color
:
COLOR
deep_pink_color
:
COLOR
pink_color
:
COLOR
light_pink_color
:
COLOR
pale_violet_red_color
:
COLOR
maroon_color
:
COLOR
medium_violet_red_color
:
COLOR
violet_red_color
:
COLOR
violet_color
:
COLOR
dark_magenta_color
:
COLOR
magenta_color
:
COLOR
dark_violet_color
:
COLOR
blue_violet_color
:
COLOR
medium_purple_color
:
COLOR
purple_color
:
COLOR
Class invariant
actions.count = elements.count