diff options
| -rw-r--r-- | generic/proof-shell.el | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 90089ebd..8ab5f328 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -178,6 +178,13 @@ If QUEUEMODE is supplied, set the lock to that value." (proof-shell-ready-prover queuemode) (setq proof-shell-error-or-interrupt-seen nil) (setq proof-shell-busy (or queuemode t)) + ;; Make modeline indicator follow state (on XEmacs at least) + (cond + (proof-running-on-XEmacs + (if (extentp (car proof-shell-active-scripting-indicator)) + (set-extent-properties + (car proof-shell-active-scripting-indicator) + '(face proof-queue-face))))) (run-hooks 'proof-state-change-hook)) (defun proof-release-lock (&optional err-or-int) @@ -185,7 +192,14 @@ If QUEUEMODE is supplied, set the lock to that value." Clear `proof-shell-busy', and set `proof-shell-error-or-interrupt-seen' to err-or-int." (setq proof-shell-error-or-interrupt-seen err-or-int) - (setq proof-shell-busy nil)) + (setq proof-shell-busy nil) + (cond + (proof-running-on-XEmacs + (if (extentp (car proof-shell-active-scripting-indicator)) + (set-extent-properties + (car proof-shell-active-scripting-indicator) + '(face proof-locked-face)))))) + @@ -356,13 +370,6 @@ of the queue region." :type 'sexp :group 'proof-general-internals) -(cond - (proof-running-on-XEmacs - (if (extentp (car proof-shell-active-scripting-indicator)) - (set-extent-properties - (car proof-shell-active-scripting-indicator) - '(face proof-locked-face))))) - (unless (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) (setq minor-mode-alist |