]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54c4126) | patch
Regression fixed: goto used to stop (again!) to the new cursor position when
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 16:32:20 +0000 (16:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 16:32:20 +0000 (16:32 +0000)
commit6ba0b48cb9e6a399d4519d40bc65a658d99a3c13
treec67b3c3bb4b866fa8fffbf66ff6b5838ff0d8825tree | snapshot
parent54c4126f4813a7ccd46ecb2155e98714261926f6commit | diff
Regression fixed: goto used to stop (again!) to the new cursor position when
the user clicks somewhere. The source of the regression was the difficulty of
remembering the position of the marks while the text is modified (by automatic
insertion of aliases). Solved by using ad-hoc temporary marks in place of
iterators (first version tried) and offsets (most recent version tried).
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.