ProofGeneral / PG

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

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

Open hendriktews opened 1 day ago

hendriktews commented 1 day ago

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 commented 1 day ago

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 commented 1 day ago

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 commented 1 day ago

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 commented 1 day ago

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 commented 19 hours ago

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 commented 18 hours ago

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 commented 11 hours ago

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 commented 3 hours ago

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 commented 3 hours ago

[...] 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.