[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: How can I undo a change from a modification-hook?
From: |
Clément Pit-Claudel |
Subject: |
Re: How can I undo a change from a modification-hook? |
Date: |
Wed, 26 Apr 2017 09:45:50 -0400 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 |
> Technically you can, but it's a bit messy and will likely not be
> 100% reliable. Personally, in your case, I wouldn't bother doing it,
> but here's how I'd do it otherwise:
Thanks for the answer! The context is Proof General: it's very annoying that
running whitespace-cleanup retracts what looks like arbitrary sections of the
buffer.
On 2017-04-26 08:26, Stefan Monnier wrote:
> [ and while
> you're there, check that the beg/end/len is within the announces
> beg/end stashed earlier, and if it's not just don't do anything
> since it means the stash buffer-undo-list is likely unrelated. ]
This part worries me. Could you clarify when this would happen?
Not doing anything is risky, because it puts the buffer in an inconsistent
state wrt the subprocess :/
Thanks!
- How can I undo a change from a modification-hook?, Clément Pit--Claudel, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/26
- Re: How can I undo a change from a modification-hook?,
Clément Pit-Claudel <=
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Clément Pit-Claudel, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Clément Pit-Claudel, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Clément Pit-Claudel, 2017/04/26
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/27
- Re: How can I undo a change from a modification-hook?, Clément Pit-Claudel, 2017/04/27
- Re: How can I undo a change from a modification-hook?, Stefan Monnier, 2017/04/27