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,


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
;;; 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
          (newarg ; Allow the user to limit the undo to the current region
            ;; 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
           "Cannot undo without retracting to the appropriate position.")))
      (undo arg))))

(defun next-undo-elt (arg)
  "Returns the undo element that will be processed on next undo/redo,
assuming the undo-in-region behavior will apply if ARG is non-nil."
  (let ((undo-list (if arg              ; handle "undo in region"
                        (region-beginning) (region-end)) ; can be '(nil)
                     buffer-undo-list)))                 ; can be nil
    (if (or (null undo-list) (equal undo-list (list nil)))
        nil                             ; there is clearly no undo elt
      (while (eq (car undo-list) nil)
        (setq undo-list (cdr undo-list))) ; get the last undo record
      (if (and (eq last-command 'undo)
               (or (eq pending-undo-list t)
                   (gethash undo-list undo-equiv-table)))
          ;; then we are within a run of consecutive undo commands
          (if (eq pending-undo-list t) nil (car pending-undo-list))
        (car undo-list)))))
ProofGeneral-devel mailing list

Reply via email to