indexing

	description: "[

		Command, which can be executed, redone, and undone.

	]"
	date: "$Date$"
	revision: "$Revision$"

deferred class

	COMMAND

feature -- Initialization

	make is
			-- Creation procedure
		deferred
		end

feature {HISTORY} -- Access

	execute (args: TUPLE) is
			-- Execute command with args.
		require
			args_not_void: args /= Void
			flags_valid: not redo_successful and not execute_successful
		deferred
		end

	undo (args: TUPLE) is
			-- Undo command
		require
			args_not_void: args /= Void
			flags_valid: redo_successful or execute_successful
		deferred
		end

	redo (args: TUPLE) is
			-- Redo command
		require
			args_not_void: args /= Void
			flags_valid: not redo_successful and not execute_successful
		deferred
		end

	name: STRING is
			-- The nama of the current command
		deferred
		end

	error_code: INTEGER

feature -- Status report

	execute_successful: BOOLEAN
			-- has the execute command been executed successfully?

	undo_successful: BOOLEAN
			-- has the undo command been executed successfully?

	redo_successful: BOOLEAN
			-- has the redo command been executed successfully?

end