diff options
| author | David Aspinall | 2002-12-29 16:18:16 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-12-29 16:18:16 +0000 |
| commit | 60594f3eae52795f82fd668c7618d6f8b12978cd (patch) | |
| tree | d80077d26fdc5df3a267c8233ca068204d5162cd | |
| parent | 862a3182bd773a798028b8703562dba27fc81f7a (diff) | |
Add followdown
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | generic/pg-user.el | 12 | ||||
| -rw-r--r-- | generic/proof-config.el | 4 |
3 files changed, 16 insertions, 5 deletions
@@ -15,6 +15,11 @@ ** Generic changes +*** Follow mode: add "followdown" setting + +In this mode, the point moves with the locked region when it moves +down in the buffer (processing). For undo, the point does not move. + *** Options and proof assistant settings improvements Facility to reset to default values added, and saving 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) |