indexing
	description: "Single-level undo mechanism"
	author: "Patrick Schoenbach"

deferred class interface
	SINGLE_LEVEL_UNDO

feature -- Measurement

	commands_remembered: INTEGER
			-- Number of commands actually remembered

	History_capacity: INTEGER is 1
			-- Capacity of command history (Always 1)
	
feature -- Status report

	end_entry
			-- Finish recording a history entry.
		require -- from UNDO_MECHANISM
			recording: is_recording
		ensure -- from UNDO_MECHANISM
			not_recording: not is_recording;


	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.
		require -- from UNDO_MECHANISM
			redoable_command: redoable;
			not_recording: not is_recording
		ensure then
			undoable: undoable

	undo
			-- Undo command.
		require -- from UNDO_MECHANISM
			undoable_command: undoable;
			not_recording: not is_recording
		require else
			undoable_or_redoable: undoable or redoable
		ensure then
			undone: old undoable implies redoable;
			redone: old redoable implies undoable
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	undoable_constraint: (undoable or redoable) implies history /= void;

end -- class SINGLE_LEVEL_UNDO