Undo Redo

Introduction

The aim of this task is to provide users with the classical undo/redo mechanism, with a user experience similar to that of other interactive programs, e.g. editors. The implementation shall reuse any available Eclipse mechanism to provide seamless integration with the platform.

The undo/redo mechanism is based on a history that records all operations performed by the user. The implementation must also provide controls such as a configuration parameter specifying the maximal size of a history.

Design

History

Firstly, we have to provide a history mechanism that allows to record a series of operations. Browsing the history should be achievable through Undo and Redo buttons, or keyboard shortcuts.

Browsing actions are context-dependent. Thus, when the user wishes to undo an operation, the latest one on the active editor must be considered. Operations must be distinguished according to the file upon which they act.

Operations

Rodin database changes must be encapsulated into operations. An operation consists in both a forward action (EXECUTE) and a backward action (UNDO), in order to restore the previous state if needed. The following invariant rules must hold:

• EXECUTE followed by UNDO is a noop
• UNDO followed by REDO is a noop

Eclipse mechanism

Eclipse provides a history mechanism, on which we lean to make the Rodin one. It offers a IOperationHistory interface, along with an implementation.

To make each editor have its own history, we could either use one history per editor, or let a single one manage all operations. As Eclipse already provides the material, we selected the second solution. Thus, before adding an operation, it is configured with a context, through the IUndoContext interface. The undo context is essentially the component name of the file being edited.

Making operations

Every user action must be covered by an operation, from the simplest (like adding an element) to more complex ones (as in wizards). The main problem in implementing a history is that we want to avoid rewriting code each time a new user action is added. This is why Operations use the Composite Pattern.

We consider five base operations on elements:

• create
• delete
• move
• copy
• change attribute

In addition to these basic operations, there are 2 operations : OperationNode and OperationCreateElement. These 2 operations are used as node in the composite Pattern. The difference is that OperationCreateElement is used to create an element with attributes.

From these operations, multiple ones can be built. For example, axiom creation is achieved by a create operation followed by two attribute modification operations (one for the label, another for the predicate).

Contributing to History

New operations are required to implement OperationTree. AtomicOperation must not be inherited. This class is only used to encapsulate operations and make them atomic.

Adding an operation to the History is achieved through the History.addOpertionHistory(AtomicOperation) method. Execution is immediate (in the same thread). Thus, created elements can be retrieved at once, if any.

Concurrency

As operations alter the database, we must avoid having several operations access the database concurrently. Therefore, OperationFactory operations are encapsulated in the AtomicOperation class that guarantees atomicity. Of course, sub-operations of a multiple operation are executed in the same thread.

The Edit menu

For Undo and Redo buttons, we use eclipse's Global Action. These are buttons and shortcuts, shared amongst several editors like undo/redo or cut/copy/paste. At every action on the history, labels are refreshed and buttons may become inactive if no more undo or redo actions remain.