indexing description: "Commands that cannot be undone" author: "Patrick Schoenbach" deferred class interface NON_UNDOABLE_COMMAND feature -- Access get_context: like context -- Returned context -- (from COMMAND_BEHAVIOR) require -- from COMMAND_BEHAVIOR context_available: context_available ensure -- from COMMAND_BEHAVIOR context_retrieved: not context_available feature -- Status report arguments_needed: BOOLEAN -- Does command need arguments? -- (from COMMAND_BEHAVIOR) arguments_set: BOOLEAN -- Are arguments set? -- (from COMMAND_BEHAVIOR) clear_history: BOOLEAN -- Shall history be cleared after execution? -- (from COMMAND_BEHAVIOR) context_available: BOOLEAN -- Is context available for retrieval? -- (from COMMAND_BEHAVIOR) context_set: BOOLEAN -- Is context set? -- (from COMMAND_BEHAVIOR) frozen Is_undoable: BOOLEAN is false valid_arguments_type (other: ANY): BOOLEAN -- Is arguments type valid? -- (from COMMAND_BEHAVIOR) valid_context_type (other: ANY): BOOLEAN -- Is context type valid? -- (from COMMAND_BEHAVIOR) feature -- Status setting set_arguments (args: CONTEXT) -- Set arguments. -- (from COMMAND_BEHAVIOR) require -- from COMMAND_BEHAVIOR valid_type: valid_arguments_type (args); arguments_not_set: not arguments_set ensure -- from COMMAND_BEHAVIOR arguments_set: arguments_set set_context (c: CONTEXT) -- Set context. -- (from COMMAND_BEHAVIOR) require -- from COMMAND_BEHAVIOR valid_type: valid_context_type (c); no_context_returned: not context_available ensure -- from COMMAND_BEHAVIOR context_set: context_set feature -- Basic operations frozen run -- Run the command. -- (from COMMAND_BEHAVIOR) require -- from COMMAND_BEHAVIOR arguments_set: arguments_set; no_context_set: not context_set; no_context_available: not context_available ensure -- from COMMAND_BEHAVIOR context_available: context_available; arguments_flag_reset: arguments_needed implies not arguments_set frozen take_back -- Take command back. -- (from COMMAND_BEHAVIOR) require -- from COMMAND_BEHAVIOR context_set: context_set ensure -- from COMMAND_BEHAVIOR no_context_set: not context_set frozen undo -- Undo command. invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); -- from COMMAND_BEHAVIOR context_availability_constraint: context_available implies not context_set; context_set_constraint: context_set implies not context_available; end -- class NON_UNDOABLE_COMMAND