indexing description: "Interface for command instances" author: "Patrick Schoenbach" deferred class interface COMMAND_INSTANCE feature -- Status report arguments_needed: BOOLEAN -- Does command need arguments? arguments_set: BOOLEAN -- Are arguments set? clear_history: BOOLEAN -- Clear history after execution? is_executed: BOOLEAN -- Has command instance been executed? is_undoable: BOOLEAN -- Is command instance undoable? feature -- Status setting set_arguments (args: ANY) -- Set arguments of command instance. require arguments_not_set: not arguments_set feature -- Basic operations execute -- Execute command instance. require not_executed: not is_executed; arguments_set: arguments_set ensure executed: is_executed redo -- Redo command instance. undo -- Undo command instance. require undoable: is_undoable; executed: is_executed ensure not_executed: not is_executed invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); argumentless_constraint: not arguments_needed implies arguments_set; end -- class COMMAND_INSTANCE