]> matita.cs.unibo.it Git - helm.git/commit
Redo fixed with a strategy similar (but not equal) to the one for undo:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 08:19:33 +0000 (08:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 08:19:33 +0000 (08:19 +0000)
commit8172bc2b4a0116f57f6f986fd5d3478c37a6598b
treeb0d8e3e3a1d5b895e27a3e3fc8b112a6c885bf65
parent4f179a8afdb2f11e669354f8fca4ffd1b0308bd2
Redo fixed with a strategy similar (but not equal) to the one for undo:
1. we save the position of all the marks
2. we redo
3. we undo
4. we save the position of the cursor after the undo
5. if necessary, we restore the initial position of all the marks,
   we move the cursor to its position after the undo and then we goto
6. we redo
helm/matita/matitaGui.ml