Dear Proof General developers,
I use extensively Coq/ProofGeneral for Emacs and I am delighted to be
able to use this wonderful tool within my favorite editor.
I have been thinking for a few days of a way to fix and improve the
`pg-protected-undo' function.
Indeed, the current implementation of pg-protected-undo which forces
undo-in-region has several bugs and/or drawbacks:
- if the size of the forced region is empty, it breaks the locked region
all the same;
- undo should be possible in the comments of the locked region (I have
just seen it is already reported by bug #294);
- since undo-in-region is forced, we cannot actually perform any
custom undo-in-region any more, and it also seems to obstruct redo;
- finally, "repetition" [when arg > 1] seems not to work properly.
I propose the enclosed Elisp code which should provide the following features:
- a safe undo function
that calls the Emacs original `undo' if there is no locked region,
else uses two auxiliary functions to get the "next undo elt" and check
it won't affect the locked region;
- if this is the case, it proposes the user (via y-or-n-p) to retract,
or do it silently if `proof-allow-undo-in-read-only' is non-nil
(thus it does not break the locked region, even if
`proof-allow-undo-in-read-only' holds);
- but the next undo/redo is always allowed if it will edit a comment;
- "custom undo in region" that could be performed by GNU Emacs undo is
still available,
- as well as "repetition" according to the given prefix argument.
Kind regards,
Erik.
PS: I tested the code with:
Coq 8.2pl2
ProofGeneral 4.0pre100709
GNU Emacs 23.2.1
--
Érik Martin-Dorel
PhD student, ENS de Lyon, LIP
erik.martin-do...@ens-lyon.org
http://perso.ens-lyon.fr/erik.martin-dorel/
;;; Copyright (c) 2010 Erik Martin-Dorel, ENS de Lyon.
;;
;; Attempt to improve `pg-protected-undo' with the help of some
;; auxiliary functions `pg-protected-undo-1' and `next-undo-elt'
;;
(defun pg-protected-undo (&optional arg)
"Provides all features of `undo' and avoids breaking the locked region.
It performs each of the desired undos thanks to `pg-protected-undo-1'
which checks that these operations will not affect the locked region.
If this is the case, it proposes the user to retract, or do it
silently if `proof-allow-undo-in-read-only' is non-nil.
Moreover, undo/redo is allowed in comments located in the locked region."
(interactive "*P")
(if (or (not proof-locked-span)
(equal (proof-queue-or-locked-end) (point-min)))
(undo arg)
(let ((repeat ; Allow the user to perform successive undos at once
(if (numberp arg)
(prefix-numeric-value arg) ; arg is a raw prefix argument
1))
(newarg ; Allow the user to limit the undo to the current region
(and
;; this Boolean expression is necessary to match
;; the behavior of GNU Emacs undo function
(or (region-active-p) (and arg (not (numberp arg
(> (region-end) (region-beginning)
(while (> repeat 0)
(pg-protected-undo-1 newarg) ; do some safe undos step by step
(setq last-command 'undo) ; need for this assignment meanwhile
(decf repeat)
(defun pg-protected-undo-1 (arg)
"This function is intended to be called by `pg-protected-undo'.
It performs a single undo/redo after checking that this operation
will not affect the locked region.
If this is the case, it proposes the user to retract, or do it
silently if `proof-allow-undo-in-read-only' is non-nil.
The flag ARG is passed to functions `undo' and `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,
;; at least for the first call from the loop of `pg-protected-undo'.
(setq arg (and arg (not (numberp arg ; ensure arg is boolean
(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
(beg (car delta))
(end (max beg (- beg (cdr delta) ; Key computation
(when (and next (> beg 0) ; the "next undo elt" exists
(> (proof-queue-or-locked-end) beg)
(not (and ; Allow undo in comments
(proof-inside-comment beg) (proof-inside-comment end
(if (or proof-allow-undo-in-read-only
(y-or-n-p "Next undo will modify read-only region, retract? "))
(proof-retract-before-change beg end)
(when (eq last-command 'undo) (setq this-command 'undo))
;; now we can stop the function without breaking possible undo chains
(error
"Cannot undo without retracting to the appropriate position.")))
(undo arg
(defun next-undo
