indexing
description: "Vision2 widget test application"
status: "See notice at end of class"
keywords: "test"
date: "$Date$"
revision: "$Revision$"
class interface
WIDGETS
create
start
main_window
feature
main_window: MAIN_WINDOW
Current
start
main_window
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
clipboard: EV_CLIPBOARD
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
contextual_help_accelerator: EV_ACCELERATOR
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result.is_equal (implementation.contextual_help_accelerator)
data: ANY
EV_ANY
help_accelerator: EV_ACCELERATOR
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result.is_equal (implementation.help_accelerator)
help_engine: EV_HELP_ENGINE
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result.is_equal (implementation.help_engine)
locked_window: EV_WINDOW
EV_WINDOWlock_update
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
windows: LINEAR [EV_WINDOW]
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result.is_equal (implementation.windows)
feature
alt_pressed: BOOLEAN
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ctrl_pressed: BOOLEAN
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
Default_tooltip_delay: INTEGER is 500
EV_APPLICATION
focused_widget: EV_WIDGET
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result = implementation.focused_widget
is_launched: BOOLEAN
launch
EV_APPLICATION
shift_pressed: BOOLEAN
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
tooltip_delay: INTEGER
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
ensure EV_APPLICATION
bridge_ok: Result = implementation.tooltip_delay
feature
set_tooltip_delay (a_delay: INTEGER)
a_delaytooltip_delay
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
a_delay_non_negative: a_delay >= 0
ensure EV_APPLICATION
assigned: tooltip_delay = a_delay
feature
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
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
display_help_for_widget (a_widget: EV_WIDGET)
a_widget
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
a_widget_not_void: a_widget /= void
enable_contextual_help
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
launch
prepare
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
not_already_launched: not is_launched
ensure EV_APPLICATION
is_launched: is_launched
process_events
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
is_launched: is_launched
sleep (msec: INTEGER)
msec
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
msec_non_negative: msec >= 0
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
set_contextual_help_accelerator (an_accelerator: EV_ACCELERATOR)
an_acceleratorcontextual_help_accelerator
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
an_accelerator_not_void: an_accelerator /= void
ensure EV_APPLICATION
contextual_help_accelerator_assigned: contextual_help_accelerator = an_accelerator
set_help_accelerator (an_accelerator: EV_ACCELERATOR)
an_acceleratorhelp_accelerator
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
an_accelerator_not_void: an_accelerator /= void
ensure EV_APPLICATION
help_accelerator_assigned: help_accelerator = an_accelerator
set_help_engine (an_engine: EV_HELP_ENGINE)
an_enginehelp_engine
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
an_engine_not_void: an_engine /= void
ensure EV_APPLICATION
help_engine_set: help_engine = an_engine
feature
do_once_on_idle (an_action: PROCEDURE [ANY, TUPLE])
an_action
EV_APPLICATION
require EV_APPLICATION
not_destroyed: not is_destroyed
drop_actions: EV_PND_ACTION_SEQUENCE
EV_APPLICATION_ACTION_SEQUENCES
ensure EV_APPLICATION_ACTION_SEQUENCES
not_void: Result /= void
idle_actions: EV_NOTIFY_ACTION_SEQUENCE
EV_APPLICATION_ACTION_SEQUENCES
ensure EV_APPLICATION_ACTION_SEQUENCES
not_void: Result /= void
pick_actions: EV_PND_ACTION_SEQUENCE
EV_APPLICATION_ACTION_SEQUENCES
ensure EV_APPLICATION_ACTION_SEQUENCES
not_void: Result /= void
post_launch_actions: EV_NOTIFY_ACTION_SEQUENCE
launch
EV_APPLICATION_ACTION_SEQUENCES
ensure EV_APPLICATION_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_APPLICATION
tooltip_delay_not_negative: tooltip_delay >= 0
windows_not_void: windows /= void
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
end -- WIDGETS