diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 21:27:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 21:27:11 +0000 |
| commit | 141b15f4ced8165116d38482a5b5f7e250ad2354 (patch) | |
| tree | 193c08335e31ba07c5260f33c409941569e5ceb0 /generic | |
| parent | cbd0e7fdfc8d92c99cb4af414e2855400423ba73 (diff) | |
Dont call dont-show-annotations for GNU Emacs to avoid nasty bug.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c1901975..2cea0c4c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1678,6 +1678,9 @@ usual, unless NOERROR is non-nil." ;;;###autoload (define-derived-mode proof-shell-mode comint-mode "proof-shell" "Proof General shell mode class for proof assistant processes" + + + (setq proof-buffer-type 'shell) ;; Clear state @@ -1698,7 +1701,12 @@ usual, unless NOERROR is non-nil." (add-hook 'comint-output-filter-functions 'proof-shell-filter nil 'local) (setq comint-get-old-input (function (lambda () ""))) - (proof-shell-dont-show-annotations) + + ;; FIXME: this is a work-around for a nasty GNU Emacs 21.2 + ;; bug which HANGS Emacs sometimes if special characters + ;; are hidden. (e.g. try M-x column-number-mode) + (unless proof-running-on-Emacs21 + (proof-shell-dont-show-annotations)) ;; Proof marker is initialised in filter to first prompt found (setq proof-marker (make-marker)) |