Undo Redo Design

Eclipse History

To implement the history, we have based mechanism History provided by Eclipse [1]. It is consist of a class History and an interface IUndoableOperation. The operations have three methods to act on the database: execute(), undo() and redo().

They are saved in the historic which call execute() for the first time and then undo () and redo () as the operation is to undo or redo.

As a file must have its own historic, the operations have a context, here it's the name of file. A History class then manages the historic of all files.

Operations

First, we have to make objects that implements IUndoableOperation for each transaction on the data base. We use the composite model so that each operation is composed of basic operations (add an element, delete an element, change an attribute ,...). The operations are created by class builder.

Some operations are dependent on an element in their execution (eg change an attibute). This may not be known when recording the operation in the History. To do this, operations have methods getCreatedElement () and setParent () which be called in execute()

Then to ensure the atomicity on the database, operations (TreeOperation) are encapsulated in a class AtomicOperation. It only delegate its methods but it encapsulates in the RodinCore.run().

Factory

The interface provides to clients consists of three class:

• OperationFactory
• History
• AtomicOperation

The factory is not instantiable and its methods are static. History implements the pattern Singleton and delegates to IOperationHistory.