indexing
description: "A keyboard accelerator defines `actions' to be performed when a`key' is pressed. See `{EV_TITLED_WINDOW}.accelerators'"
status: "See notice at end of class"
keywords: "accelerator, keyboard, key, shortcut, hotkey"
date: "$Date$"
revision: "$Revision$"
class interface
EV_ACCELERATOR
create
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
make_with_key_combination (a_key: EV_KEY; require_control, require_alt, require_shift: BOOLEAN)
a_key
require
a_key_not_void: a_key /= void
feature
alt_required: BOOLEAN
actions
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.alt_required
control_required: BOOLEAN
actions
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.control_required
data: ANY
EV_ANY
key: EV_KEY
actions
require
not_destroyed: not is_destroyed
ensure
bridge_ok: equal (Result, implementation.key)
parented: BOOLEAN
Current
Current
Current
require
not_destroyed: not is_destroyed
shift_required: BOOLEAN
actions
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.shift_required
feature
is_equal (other: like Current): BOOLEAN
otherCurrent
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
out: STRING
feature
disable_alt_required
alt_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
not_alt_required: not alt_required
disable_control_required
control_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
not_control_required: not control_required
disable_shift_required
shift_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
not_shift_required: not shift_required
enable_alt_required
alt_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
alt_required: alt_required
enable_control_required
control_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
control_required: control_required
enable_shift_required
shift_required
require
not_destroyed: not is_destroyed
not_parented: not parented
ensure
shift_required: shift_required
set_key (a_key: EV_KEY)
a_keykey
require
not_destroyed: not is_destroyed
a_key_not_void: a_key /= void
not_parented: not parented
ensure
a_key_assigned: key.is_equal (a_key)
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
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
actions: EV_NOTIFY_ACTION_SEQUENCE
Current
require
not_destroyed: not is_destroyed
ensure
result_not_void: Result /= void
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
key_not_void: key /= void
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
end -- EV_ACCELERATOR