leanprover
Eager replacement of abbreviations destroys redo history
Consider the following input:
foo bar \n foo bar
where the \n is typed in as \\n.
When using undo to return the document to an empty state and then using redo, the extension eagerly replaces \n with ¬, destroying the rest of the redo history (in this case the bar).
Sorry for not answering earlier, I wasn't aware of this issue. The underlying issue is that the rewrite feature does not distinguish between user edits and edits caused by redo/undo. They need to be distinguished. Sadly, VS Code does not seem to indicate whether a text change is caused by a redo or by the user.
It only happens though if the leader character is inserted by redo.
A perfect implementation of the rewrite feature would always have this issue, regardless of eager replacement. "Luckily" VS Code aggregates undos/redos into whole word edits. The current rewrite feature implementation is only triggered by a single-character text change that inserts \ (assuming that if the user types \alpha very quickly, it still emits a single text change event for \).
Maybe disabling undo stops before/after the abbreviation is replaced could fix this particular case.
The flag is now available in the latest release: https://code.visualstudio.com/updates/v1_59#_text-document-change-reason
It just needs to be adopted.