indexing description: "Multi-level undo mechanism" author: "Patrick Schoenbach" deferred class interface MULTI_LEVEL_UNDO feature -- Measurement commands_remembered: INTEGER -- Number of commands actually remembered history_capacity: INTEGER -- Capacity of command history feature -- Status report is_recording: BOOLEAN -- Is mechanism recording a history entry at the moment? -- (from UNDO_MECHANISM) redoable: BOOLEAN -- Is there a redoable command in the history? undoable: BOOLEAN -- Is there an undoable command in the history? feature -- Basic operations redo -- Redo command. -- (from UNDO_MECHANISM) require -- from UNDO_MECHANISM redoable_command: redoable; not_recording: not is_recording undo -- Undo command. -- (from UNDO_MECHANISM) require -- from UNDO_MECHANISM undoable_command: undoable; not_recording: not is_recording invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); history_exists: history /= void; end -- class MULTI_LEVEL_UNDO