diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2012-05-31 14:39:33 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2012-05-31 14:39:33 +0000 |
| commit | d248f8dfe716749c98143c9bb33dc28e79196d5f (patch) | |
| tree | ff952de1be6260e05b8cddd206ff7286334592bc /generic/pg-user.el | |
| parent | 56f018fbcf5ee07eee3a0a463084446fef52415c (diff) | |
let proof-retract-buffer only move point when called interactively
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index e08d7f0c..8a5675fc 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -245,14 +245,20 @@ the text region in the proof script after undoing." (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))) -(defun proof-retract-buffer () - "Retract the current buffer, and maybe move point to the start." - (interactive) +(defun proof-retract-buffer (&optional called-interactively) + "Retract the current buffer, and maybe move point to the start. +Point is only moved according to `proof-follow-mode', if +CALLED-INTERACTIVELY is non-nil, which is the case for all +interactive calls." + ;; The numeric prefix argument "p" is never nil, + ;; see Section "Distinguish Interactive Calls" in the Elisp manual. + (interactive "p") (proof-with-script-buffer (save-excursion (goto-char (point-min)) (proof-retract-until-point-interactive)) - (proof-maybe-follow-locked-end (point-min)))) + (if called-interactively + (proof-maybe-follow-locked-end (point-min))))) (defun proof-retract-current-goal () "Retract the current proof, and move point to its start." |