Fixed requires for FSF Emacs.

Patched (old bug?) in proof-response-buffer-display, how did it
come back?

2 files changed, 13 insertions, 5 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 38c66487..8fabb2b8 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -20,7 +20,7 @@
 
 ;; Nuke some byte-compiler warnings
 (eval-when-compile
-  (require 'func-menu)
+  (if (locate-library "func-menu") (require 'func-menu))
   (require 'comint))
 
 ;; FIXME:
@@ -299,7 +299,8 @@ to allow other files loaded by proof assistants to be marked read-only."
 	  (and buffer
 	       (buffer-modified-p buffer)
 	       (proof-warning (concat "Changes to "
-				      (buffer-name buffer) " have not been saved!")))
+				      (buffer-name buffer)
+				      " have not been saved!")))
 	  (setq proof-included-files-list
 		(cons cfile proof-included-files-list))
 	  ;; If the file is loaded into a buffer, which isn't
diff --git a/generic/proof.el b/generic/proof.el
index c57ca087..16149937 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -19,8 +19,11 @@
 
 (require 'proof-splash)			; splash screen
 
+;; cl is dumped with my XEmacs 20.4, but not FSF Emacs 20.2.
+(require 'cl)				
+
+
 ;; FIXME da: I think these should all be autoloaded!!
-;; (require 'cl)
 ;; (require 'compile)
 ;; (require 'comint)
 ;; (require 'etags)			
@@ -92,8 +95,12 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
       (set-buffer proof-response-buffer)
       (setq start (goto-char (point-max)))
       (insert str)
-      (font-lock-fontify-region start (point-max))
-      (font-lock-append-text-property start (point-max) 'face face)
+      ;; FIXME da: recurring bug here???
+      (if (string-match "XEmacs" emacs-version)
+	  (progn
+	    (font-lock-fontify-region start (point-max))
+	    (font-lock-append-text-property start (point-max) 'face face)))
+      ;; 
       (insert "\n"))))
 
 ;;;