Add followdown

2 files changed, 11 insertions, 5 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 146a5206..27adf37f 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -24,10 +24,14 @@
 	,@body)))
 
 (defun proof-maybe-follow-locked-end ()
-  "Maybe point to the make sure the locked region is displayed."
-  (if (eq proof-follow-mode 'follow)
-    (proof-goto-end-of-queue-or-locked-if-not-visible)))
-
+  "Maybe move point to make sure the locked region is displayed."
+  (cond
+   ((eq proof-follow-mode 'follow)
+    (proof-goto-end-of-queue-or-locked-if-not-visible))
+   ((eq proof-follow-mode 'followdown)
+    (if (> (proof-queue-or-locked-end) (point))
+	(goto-char (proof-queue-or-locked-end))))))
+	
 
 ;;
 ;; Doing commands
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 777fd66c..3d99e727 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -333,16 +333,18 @@ releases and turned off in stable releases."
 
 (defcustom proof-follow-mode 'locked
   "*Choice of how point moves with script processing commands.
-One of the symbols: 'locked, 'follow, 'ignore.
+One of the symbols: 'locked, 'follow, 'followdown, 'ignore.
 
 If 'locked, point sticks to the end of the locked region.
 If 'follow, point moves just when needed to display the locked region end.
+If 'followdown, point if necessary to stay in writeable region
 If 'ignore, point is never moved after movement commands or on errors.
 
 If you choose 'ignore, you can find the end of the locked using
 `M-x proof-goto-end-of-locked'."
   :type '(choice
 	  (const :tag "Follow locked region" locked)
+	  (const :tag "Follow locked region down" followdown)
 	  (const :tag "Keep locked region displayed" follow)
 	  (const :tag "Never move" ignore))
   :group 'proof-user-options)