indexing
	description: "General undo mechanism"
	author: "Patrick Schoenbach"

deferred class interface
	UNDO_MECHANISM

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?

	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.
		require
			redoable_command: redoable;
			not_recording: not is_recording

	undo
			-- Undo command.
		require
			undoable_command: undoable;
			not_recording: not is_recording
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	behavior_table_exists: commands /= void;
	entry_list_exists: entry_list /= void;
	no_undefined_command_slots: commands.full;
	entry_list_constraint: not is_recording implies entry_list.empty;

end -- class UNDO_MECHANISM