branch: scratch/proof-general
commit ef92861928da68f777ef6c583d18e581e4e9ffb1
Author: Stefan Monnier <monn...@iro.umontreal.ca>
Commit: Stefan Monnier <monn...@iro.umontreal.ca>
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`.
---
generic/pg-user.el | 26 ++++++++++++++++----------
1 file changed, 16 insertions(+), 10 deletions(-)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 07ff560fba..b47f770cab 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2019 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2024 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -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)
@@ -1609,10 +1609,19 @@ the locked region."
(setq last-command 'undo) ; need for this assignment meanwhile
(cl-decf repeat)))))
+(defalias 'pg--undo-delta
+ (if (equal '(13 . 21) (undo-delta '(apply 21 13 57 fun arg1))) ;Emacs-31
+ #'undo-delta
+ (lambda (elt)
+ (pcase elt
+ ((and `(apply ,delta ,beg . ,_) (guard (integerp delta)))
+ (cons beg delta))
+ (_ (undo-delta elt))))))
+
(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,8 +1630,8 @@ 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))
- (delta (undo-delta next)) ; can be '(0 . 0) if next is nil
+ (let* ((next (pg--next-undo-elt arg))
+ (delta (pg--undo-delta next)) ; can be '(0 . 0) if next is nil
(beg (car delta))
(end (max beg (- beg (cdr delta))))) ; Key computation
(when (and next (> beg 0) ; the "next undo elt" exists
@@ -1640,7 +1649,7 @@ 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"
@@ -1650,10 +1659,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 '(0 . 0) (pg--undo-delta (car undo-list)))))
(setq undo-list (cdr undo-list))) ; get the last undo record
(if (and (eq last-command 'undo)
(or (eq pending-undo-list t)
