aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el18
1 files changed, 11 insertions, 7 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 862c92bf..448b3691 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1560,9 +1560,20 @@ No action if BUF is nil."
;; Active terminator minor mode ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; FIXME: Paul Callaghan wants to make the default for this be
+;; 't'. Perhaps we need a user option which configures the default.
+;; Moreover, this minor mode is only relevant to scripting
+;; buffers, so a buffer-local setting may be inappropriate.
(deflocal proof-active-terminator-minor-mode nil
"Active terminator minor mode flag")
+;; Make sure proof-active-terminator-minor-mode is registered
+(or (assq 'proof-active-terminator-minor-mode minor-mode-alist)
+ (setq minor-mode-alist
+ (append minor-mode-alist
+ (list '(proof-active-terminator-minor-mode
+ (concat " " proof-terminal-string))))))
+
(defun proof-active-terminator-minor-mode (&optional arg)
"Toggle Proof General's active terminator minor mode.
With ARG, turn on the Active Terminator minor mode if and only if ARG
@@ -1572,13 +1583,6 @@ If active terminator mode is enabled, pressing a terminator will automatically a
(interactive "P")
-;; has this minor mode been registered as such?
- (or (assq 'proof-active-terminator-minor-mode minor-mode-alist)
- (setq minor-mode-alist
- (append minor-mode-alist
- (list '(proof-active-terminator-minor-mode
- (concat " " proof-terminal-string))))))
-
(setq proof-active-terminator-minor-mode
(if (null arg) (not proof-active-terminator-minor-mode)
(> (prefix-numeric-value arg) 0)))