From 141b15f4ced8165116d38482a5b5f7e250ad2354 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 18 Jul 2002 21:27:11 +0000
Subject: Dont call dont-show-annotations for GNU Emacs to avoid nasty bug.

---
 generic/proof-shell.el | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'generic/proof-shell.el')

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))
-- 
cgit v1.2.3