| | | B.2.4 undo, redo: Undo/Redo Proof Commands |
undo
undo S
redo
: undo
: redo
In proving mode.
The command undo cancels the effect of the proof command that was executed in the parent of the current state; it re-opens the parent state (discarding all its child states) and makes it the new current state.
If the optional state label S is provided, it must denote some ancestor of the current state, i.e., some state on the path from the parent of the current state to the root of the proof tree. Then the command cancels the effects of all proof commands along this path such that the ancestor is re-opened and becomes the new current state. Thus the effect of this form of the command is the same as if just undo is executed multiple times until the ancestor is reached.
If a state is re-opened by applying undo, it internally still retains its discarded child states unless another application of a proof command generates new child states. Until this is the case, an application of redo is able to restore the subtree rooted in the current proof state to its shape before the application of undo that re-opened the current state (however, the new current state after a redo need not be the the same as the current state before the undo but may be just a sibling of it). A repeated application of redo along a path of proof states in which undo was applied thus restores the situation before these applications.
A user may want to discard an unsuccessful proof branch by multiple applications of undo but accidentally performs one undo too much, such that the parent state of the unsuccessful branch is re-opened and also all other (potentially successful) sibling branches are discarded. Then the user only needs to apply redo once to restore the accidentally discarded branches. If the user also wishes to re-store the unsuccessful branch, she just has to go to the root state of that branch and continue there with the application of redo.
| | | B.2.4 undo, redo: Undo/Redo Proof Commands |