From d248f8dfe716749c98143c9bb33dc28e79196d5f Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Thu, 31 May 2012 14:39:33 +0000
Subject: let proof-retract-buffer only move point when called interactively

---
 generic/pg-user.el | 14 ++++++++++----
 1 file 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."
-- 
cgit v1.2.3