ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
492 stars 89 forks source link

Task: improve/harden the pg-protected-undo function #803

Open erikmd opened 4 days ago

erikmd commented 4 days ago

I had refactored PG's behavior w.r.t. C-_ a long time ago (which was fairly broken before my patches)

There is a limitation of the current algorithm of "pg-protected-undo":

  1. one idea of this feature is that PG retracts by defaults, except when one edits just inside a comment
  2. this idea applies as well if we kill a region within a single comment
  3. but the implementation of this idea was done so that it just checks whether the first char and the last char are within comments
  4. as a result, the limitation is that "if we kill a region that spans over two distinct comments", then it doesn't retract (while it should, as we removed text from the comments and some *) (* chars...)

FTR: see also https://github.com/ProofGeneral/PG/issues/800

monnier commented 4 days ago

My suggestion in Issue#800 was probably naive. I think the problem is more subtle because when we undo a deletion of "foo ) bar ( baz" it means we'll add this string, but we can't figure out whether this undo will change non-comment code without a much finer analysis (in the general case we'll need to compare the code after the undo).