indexing
description: "Execute commands."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_COMMAND_EXEC
create
make (a_command: WEL_COMMAND; an_argument: ANY)
commandargument
a_commandan_argument
require
a_command_not_void: a_command /= void
ensure
command_set: command = a_command
argument_set: argument = an_argument
feature
make (a_command: WEL_COMMAND; an_argument: ANY)
commandargument
a_commandan_argument
require
a_command_not_void: a_command /= void
ensure
command_set: command = a_command
argument_set: argument = an_argument
feature
argument: ANY
command
command: WEL_COMMAND
feature
execute (window: WEL_WINDOW; message, wparam, lparam: INTEGER)
message
command
require
window_not_void: window /= void
positive_message: message >= 0
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_COMMAND_EXEC