query-replace inside the processed region selects the first match, rather than the next one

[proofgeneral]

query-replace inside the processed region selects the first match, rather than the next one

[hendriktews]

This sounds like retraction is moving point around. We should eventually fix this. H.

[Matafou]

Strange bug. Retraction seems correctly protected against that. Strangely
enough it does not seem to got exactly to the top of the buffer (misses
first lines).

Looks like a specific bad interaction with query-replace.

P.

2016-01-25 11:59 GMT+01:00 hendriktews [email protected]:

This sounds like retraction is moving point around. We should
eventually fix this.

H.

—
Reply to this email directly or view it on GitHub
#41 (comment).

[erikmd]

Hello,
I've just looked at this issue, and found that enclosing the end of function proof-retract-before-change in a (save-match-data &rest BODY) successfully protects retraction with respect to query-replace and replace-string. So I'm going to push my patch and close the issue.
Best regards, EMD