]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83f44ff) | patch
Bug fix: undo now respects the locked area.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 19 Jul 2005 17:22:14 +0000 (17:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 19 Jul 2005 17:22:14 +0000 (17:22 +0000)
commit5022202a659044d981833ba8665424a52684b07f
treeae0f258c06c22880feabaacd95423fb7096bb586tree | snapshot
parent83f44ffec0422dbad242b56d651a6e56ce24ddd8commit | diff
Bug fix: undo now respects the locked area.
Algorithm to fix the bug:
 1. save the status of all the marks
 2. undo
 3. save the status of the cursor after the undo
 4. redo
 5. restore the status of all the marks
 6. if necessary, move the cursor back to its position after the undo
    and perform a goto to unlock the area
 7. perform the undo again

The same algorithm should be applied again to the redo operation!
helm/matita/matitaGui.ml diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
helm/matita/matitaScript.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.