undo does not retract when undoing a comment created by comment-dwim

[hendriktews]

to reproduce

Definition a := 1.

Definition b := 2.

(*
- mark whole line of definition b 
- do comment-dwim (M-;)
- process whole file, including this comment
- undo via keybinding to run the remapping pg-protected-undo

can be reproduced with comment-style set to 'extra-line and 'indent
*)

[hendriktews]

AFAICT the problem is that comment-dwim creates an undo group (i.e., the car of buffer-undo-list is nil), so next-undo-elt returns this nil and then the when in pg-protected-undo-1 skips over the logic that triggers retraction. Most of the code is from @DavidAspinall from 2010 with some additions from @erikmd from 2018. Does anybody know whether change groups existed already in 2010 or were ever considered when writing/updating pg-protected-undo?

[monnier]

additions from @erikmd from 2018. Does anybody know whether change groups existed already in 2010 or were ever considered when writing/updating `pg-protected-undo`?

They did exist: commit 69cae2d4bf5ef048ae933a49e64258d4a7b4fc99 Author: Richard M. Stallman ***@***.***> Date: Wed Feb 6 15:20:36 2002 +0000 (atomic-change-group, prepare-change-group, activate-change-group) (accept-change-group, cancel-change-group): New functions. and I definitely knew about them back then, but they are/were not used very often. I suspect the fix is simply to skip any leading undo boundary at the beginning of the function, just like `undo` does: ;; Strip any leading undo boundaries there might be, like we do ;; above when checking. (while (eq (car list) nil) (setq list (cdr list))) [ tho I now see that this loop is dangerous since it inf-loops when `list` is nil. I wonder why we never hit that snag in `undo`. ]

[hendriktews]

OK, thanks for the explanation!
My understanding from the elisp manual is that undo groups are enclosed within nil elements with all the n elements of the group before the next nil, where, in general n > 1. If you only split the leading nil, you would break the group, wouldn't you?

[monnier]

My understanding from the elisp manual is that undo groups are enclosed
within nil elements with all the n elements of the group before the next
nil, where, in general n > 1.

That's right.
[ And this is the case for "undo groups" in general, atomic groups are
not directly related to it, other than the fact that the implementation
uses such nil boundaries. ]

Tho IIRC n can be 0.

If you only split the leading nil, you would break the group,
wouldn't you?

I'm not sure what you mean by "split the .. nil" but in any case,
according to what I see the problem is that next-undo-elt (which
really should be renamed so as not to step on the global
namespace) doesn't know about the apply undo elements and neither does
undo-delta.

IOW, I get the expected behavior with the patches below:

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 07ff560fba..a009c91e14 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1569,7 +1569,7 @@ removed if it matches the last item in the ring."
 ;; `buffer-undo-list' in `proof-set-queue-endpoints'.
 ;;
 ;; Improved version due to Erik Martin-Dorel.  Uses auxiliary
-;; functions `pg-protected-undo-1' and `next-undo-elt'
+;; functions `pg-protected-undo-1' and `pg--next-undo-elt'
 ;;
 
 (define-key proof-mode-map [remap undo] 'pg-protected-undo)
@@ -1612,7 +1612,7 @@ the locked region."
 (defun pg-protected-undo-1 (arg)
   "This function is intended to be called by `pg-protected-undo'.
 
-The flag ARG is passed to functions `undo' and `next-undo-elt'.
+The flag ARG is passed to functions `undo' and `pg--next-undo-elt'.
 It should be a non-numeric value saying whether an undo-in-region
 behavior is expected."
 ;; Note that if ARG is non-nil, (> (region-end) (region-beginning)) must hold,
@@ -1621,7 +1621,7 @@ behavior is expected."
   (if (or (not proof-locked-span)
 	  (equal (proof-queue-or-locked-end) (point-min))) ; required test
       (undo arg)
-    (let* ((next (next-undo-elt arg))
+    (let* ((next (pg--next-undo-elt arg))
 	   (delta (undo-delta next))  ; can be '(0 . 0) if next is nil
 	   (beg (car delta))
 	   (end (max beg (- beg (cdr delta))))) ; Key computation
@@ -1640,20 +1640,20 @@ behavior is expected."
 	   "Cannot undo without retracting to the appropriate position")))
       (undo arg))))
 
-(defun next-undo-elt (arg)
+(defun pg--next-undo-elt (arg)
   "Return the undo element that will be processed on next undo/redo.
 Assume the undo-in-region behavior will apply if ARG is non-nil."
   (let ((undo-list (if arg		; handle "undo in region"
 		       (undo-make-selective-list
 			(region-beginning) (region-end)) ; can be '(nil)
 		     buffer-undo-list)))		 ; can be nil
-    (if (or (null undo-list) (equal undo-list (list nil)))
+    (if (member undo-list '(nil (nil)))
 	nil				; there is clearly no undo elt
       (while (and undo-list             ; to ensure it will terminate
-                  (let ((elt (car undo-list)))
-                    (not (and (consp elt)
-                              (or (stringp (car elt))
-                                  (integerp (car elt)))))))
+                  (let ((elt (car-safe (car undo-list))))
+                    (not (or (stringp elt)
+                             (integerp elt)
+			     (eq 'apply elt)))))
 	(setq undo-list (cdr undo-list))) ; get the last undo record
       (if (and (eq last-command 'undo)
 	       (or (eq pending-undo-list t)

and

diff --git a/lisp/simple.el b/lisp/simple.el
index 3a142ef14b3..a8a18f428d9 100644
--- a/lisp/simple.el
+++ b/lisp/simple.el
@@ -3993,6 +3993,8 @@ undo-delta
 	    ((integerp (car undo-elt))
 	     ;; (BEGIN . END)
 	     (cons (car undo-elt) (- (car undo-elt) (cdr undo-elt))))
+            ((and (eq 'apply (car undo-elt)) (numberp (nth 1 undo-elt)))
+             (cons (nth 2 undo-elt) (nth 1 undo-elt)))
 	    (t
 	     '(0 . 0)))
     '(0 . 0)))

[hendriktews]

Thanks a lot for the patch! I will transform it into a PR after I added some tests that check for this issue.

I'm not sure what you mean by "split the .. nil" but in any case,

Let's drop this, it's probably a misunderstanding on my side.

[monnier]

Thanks a lot for the patch! I will transform it into a PR after I added some tests that check for this issue.

Looking at the code, I think `(pg--)next-undo-elt` would gain by using `undo-delta` *instead* of testing `string/integerp`: diff --git a/generic/pg-user.el b/generic/pg-user.el index 07ff560fba..4c49af244b 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1650,10 +1650,7 @@ Assume the undo-in-region behavior will apply if ARG is non-nil." (if (or (null undo-list) (equal undo-list (list nil))) nil ; there is clearly no undo elt (while (and undo-list ; to ensure it will terminate - (let ((elt (car undo-list))) - (not (and (consp elt) - (or (stringp (car elt)) - (integerp (car elt))))))) + (not (equal (undo-delta (car undo-list)) '(0 . 0)))) (setq undo-list (cdr undo-list))) ; get the last undo record (if (and (eq last-command 'undo) (or (eq pending-undo-list t) and actually once you do thatm you can simplify the code further by making it return not the undo element but the `undo-delta` (since the caller only needs the delta). Note that one of my previous patches touches `lisp/simple.el`, i.e. is a patch to Emacs rather than to PG. So we should `M-x report-emacs-bug` for it, and in the mean time use some kind of workaround in our code.

[erikmd]

Hi @hendriktews,

Thanks for the ping, indeed I had refactored C-_ feature a while ago (which was fairly broken before my patches)

I'd like to let you know that I was aware of a limitation of the current algorithm of the pg-protected-undo feature:

1. the idea is that current PG doesn't retract by default whether 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...)

@monnier I didn't took a close look at your patches, but maybe you straightforwardly fixed 4 ?

[hendriktews]

Hi Erik,
I read about this limitation when I debugged this issue and this limitation is not causing this issue. The root cause of this issue is that PG's undo logic does not properly handle undo groups.

[hendriktews]

[...] is a patch to Emacs rather than to PG. So we should M-x report-emacs-bug for it, and in the mean time use some kind of workaround in our code.

OK, didn't see this before. With our current Emacs support policy the workaround needs to live about a decade.

[monnier]

@monnier I didn't took a close look at your patches, but maybe you straightforwardly fixed 4 ?

No, the limitation you mention still applies, my patch attacks another problem which is that both our undo code and part of Emacs's undo code fail to take into account a specific kind of undo element. These elements were introduced back in Emacs-22 but they're used fairly rarely, tho `comment-dwim` started to use it recentlyish making them more common.

[monnier]

OK, didn't see this before. With our current Emacs support policy the workaround needs to live about a decade.

Yup, but I think the workaround can be clean and simple enough. I hope I'll have time to provide an overall patch this week-end or early next week.

[hendriktews]

On 2024-11-22 06:27:21, monnier ***@***.***> wrote: I hope I'll have time to provide an overall patch this week-end or early next week.

Thanks for this commitment. I'll focus on some tests then. It would be nice, if you could file that bug against Emacs, because it would take me a while to create a proper one.

[erikmd]

OK great! Thanks Hendrik and Stefan!

BTW, if you think it's worth it (?), I could open another issue to track the "limitation" I've just talked about… as I'll be willing to look at this anew later on, trying to fix the issue thoroughly.

[monnier]

BTW, if you think it's worth it (?), I could open another issue to track [the "limitation"](#800 (comment)) I've just talked about…

Please do.

as I hope to be able to properly fix this soonish

I suspect it could be as simple as (save-excursion (goto-char (or (nth 8 (syntax-ppss beg)) beg)) (forward-comment (point-max)) (>= (point) end))

[monnier]

I pushed to nongnu.git a branch scratch/proof-general with three commits:

commit 83ba6139623b9011e87abeccc0c4d6f680464b42 (HEAD -> elpa/proof-general)
Author: Stefan Monnier <[email protected]>
Date:   Sat Nov 23 21:43:35 2024 -0500

    pg-user.el: Misc cleanups from compilation warnings
    
    * generic/pg-user.el: Fix docstring markup warnings.
    Avoid `point-at-eol`, declared obsolete in Emacs-29.
    Prefer #' to quote function names.
    (proof-electric-terminator-enable): Add FIXMEs.
    (proof-check-annotate-source): Pass 2nd arg to `looking-back` to try
    and avoid pathological behaviors (and silence a warning).
    (proof-check-generate-report): Add FIXME about use of `coq-*` variable
    in this generic files.
    (proof-autosend-loop-all, proof-autosend-loop-next):
    Remove `unwind-protect` used without any unwind form.

commit 73c13d63d9c0dae5df00ade7cd8dfabef76fb11f
Author: Stefan Monnier <[email protected]>
Date:   Sat Nov 23 21:21:36 2024 -0500

    Simplify code of `pg-protected-undo`
    
    The last change made `undo-delta` be used at two places very close
    to each other, so consolidate the two calls.  Change the test
    order since in the case where `(eq last-command 'undo)` we ended up
    throwing away the work we'd just done and then returning the
    first element without checking that its delta is non-trivial.
    
    * generic/pg-user.el (pg--next-undo-delta): Rename from
    `pg--next-undo-elt`.  Make it check `last-command` at the beginning
    rather than at the end.  Make it return the delta rather than the elt.
    Don't bother special-casing `nil` and `(nil)`.
    (pg-protected-undo-1): Adjust accordingly.

commit 7567ac4a2575f1a4d0df525d8b02946ad66496b0
Author: Stefan Monnier <[email protected]>
Date:   Sat Nov 23 20:59:09 2024 -0500

    Try and fix Issue #800
    
    `next-undo-elt` incorrectly skipped `apply` elements, and moreover
    Emacs's own `undo-delta` does not handle such elements correctly
    either.
    Hopefully `undo-delta` will be fixed in Emacs-31, but in the mean time,
    use our own function instead.  Also fix `next-undo-elt` by making
    it use `undo-delta` instead of re-implementing part of it.
    Give it a proper namespace prefix while we're at it.
    
    * generic/pg-user.el (pg--undo-delta): New function.
    (pg-protected-undo-1): Use it.
    (pg--next-undo-elt): Rename from `next-undo-elt`.  Use `pg--undo-delta`.

This requires more tests, tho. Only one of the commits actually fixes the problem.
The other two are followon cleanups.

You can get the branch with something like:

git remote add -f -t scratch/proof-general elpa git://git.sv.gnu.org/emacs/nongnu.git

[monnier]

BTW, the problem in undo-delta is now fixed in Emacs's master branch (i.e. will be fixed in Emacs-31).