More fixes for cleaner byte compile.

2 files changed, 10 insertions, 10 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 5e13be05..690eda08 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -14,7 +14,7 @@
 (require 'proof-indent)
 
 ;; Spans are our abstraction of extents/overlays.
-(eval-when-compile
+(eval-and-compile
   (cond ((fboundp 'make-extent) (require 'span-extent))
 	((fboundp 'make-overlay) (require 'span-overlay))))
 
@@ -33,7 +33,8 @@
 	  '(proof-shell-ready-prover
 	    proof-start-queue
 	    proof-shell-live-buffer
-	    proof-shell-invisible-command)))
+	    proof-shell-invisible-command
+	    proof-response-buffer-display)))
 
 ;;
 ;;  Internal variables used by script mode
@@ -1372,6 +1373,7 @@ sent to the assistant."
 ;; configuring for new assistants.
 
 ;;;###autoload
+(eval-and-compile			; to define vars
 (define-derived-mode proof-mode fundamental-mode 
   proof-mode-name
   "Proof General major mode class for proof scripts.
@@ -1386,7 +1388,7 @@ sent to the assistant."
   (add-hook 'kill-buffer-hook
 	    (lambda ()
 	      (setq proof-script-buffer-list
-		    (remove (current-buffer) proof-script-buffer-list)))))
+		    (remove (current-buffer) proof-script-buffer-list))))))
 
 ;; Fixed definitions in proof-mode-map, which don't depend on
 ;; prover configuration.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a945fb5f..476145b7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -15,14 +15,10 @@
 
 (eval-when-compile
   (require 'comint)
-  (require 'font-lock))
-
-;; Spans are our abstraction of extents/overlays.
-(eval-when-compile
+  (require 'font-lock)
   (cond ((fboundp 'make-extent) (require 'span-extent))
 	((fboundp 'make-overlay) (require 'span-overlay))))
 
-
 ;; FIXME:
 ;; Autoloads for proof-script (added to nuke warnings,
 ;; maybe should be 'official' exported functions in proof.el)
@@ -944,6 +940,7 @@ how far we've got."
 ;; OLD COMMENT: "This has to come after proof-mode is defined"
 
 ;;###autoload
+(eval-and-compile			; to define vars
 (define-derived-mode proof-shell-mode comint-mode 
   "proof-shell" "Proof General shell mode class for proof assistant processes"
   (setq proof-buffer-type 'shell)
@@ -975,7 +972,7 @@ how far we've got."
   (setq proof-re-term-or-comment 
 	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
 		"\\|" (regexp-quote proof-comment-end)))
-  )
+  ))
 
 
 (easy-menu-define proof-shell-menu
@@ -1008,6 +1005,7 @@ how far we've got."
 	()
       (error "Failed to initialise proof process"))))
 
+(eval-and-compile			; to define vars
 (define-derived-mode pbp-mode fundamental-mode 
   proof-mode-name "Proof by Pointing"
   ;; defined-derived-mode pbp-mode initialises pbp-mode-map
@@ -1015,7 +1013,7 @@ how far we've got."
   (suppress-keymap pbp-mode-map 'all)
   ;; (define-key pbp-mode-map [(button2)] 'pbp-button-action)
   (proof-define-keys pbp-mode-map proof-universal-keys)
-  (erase-buffer))
+  (erase-buffer)))