Fix a few compiler warnings

4 files changed, 28 insertions, 17 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 9c7365bc..df1cece2 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -12,6 +12,10 @@
 
 (require 'pg-assoc)
 
+;; Nuke some byte compiler warnings.
+(eval-when-compile
+  (require 'easymenu))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Goals buffer mode
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index d9992ff6..ea700deb 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -142,18 +142,18 @@ If in three window or multiple frame mode, display two buffers."
 ;;;###autoload
 (defun proof-menu-define-specific ()
   (easy-menu-define 
-   proof-assistant-menu 
-   proof-mode-map
+    proof-assistant-menu 
+    proof-mode-map
     (concat "The menu for " proof-assistant)
     (cons proof-assistant
-	   (append
-	    (proof-ass menu-entries)
-	    '("----")
-	    (or proof-menu-favourites
-		(proof-menu-define-favourites-menu))
-	    (or proof-menu-settings
-		(proof-menu-define-settings-menu))
-	    '("----")
+	    (append
+	     (proof-ass menu-entries)
+	     '("----")
+	     (or proof-menu-favourites
+		 (proof-menu-define-favourites-menu))
+	     (or proof-menu-settings
+		 (proof-menu-define-settings-menu))
+	     '("----")
 	    (list
 	     (vector
 	      (concat "Start " proof-assistant)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 8dc26f9a..d7a05cf4 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -10,11 +10,22 @@
 
 (require 'proof-menu)
 (require 'span)
-(require 'pg-goals)			; associated output
+
+;;
+;; Internal variables used in sub-modules
+;;
+
+;; A raw record of the last output from the proof system
+(defvar proof-shell-last-output nil
+  "A record of the last string seen from the proof system.")
+
+
+;; sub-modules
+
 (require 'pg-response)			; buffers for goals/response
+(require 'pg-goals)			; associated output
 
 ;; Nuke some byte compiler warnings.
-
 (eval-when-compile
   (require 'comint)
   (require 'font-lock))
@@ -78,10 +89,6 @@ See the functions `proof-start-queue' and `proof-exec-loop'.")
   "A record of the last prompt seen from the proof system.
 This is the string matched by `proof-shell-annotated-prompt-regexp'.")
 
-;; A raw record of the last output from the proof system
-(defvar proof-shell-last-output nil
-  "A record of the last string seen from the proof system.")
-
 ;; A flag indicating the type of thing proof-shell-last-output
 (defvar proof-shell-last-output-kind nil
   "A symbol denoting the type of the last output string from the proof system.
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 08da16b3..36a04458 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -347,7 +347,7 @@ Behaviour is still worse than before."
 	       (fold-spans-aux f (span-property l 'before) FROM MAPARGS)))
 	(t ())))
 
-(defun fold-spans (f &optional BUFFER FROM TO DUMMY1 DUMMY2 DUMMY3)
+(defun fold-spans (f &optional BUFFER FROM TO DUMMY1 DUMMY2 DUMMY3 DUMMY4)
   (save-excursion
     (set-buffer (or BUFFER (current-buffer)))
     (car (or (last (fold-spans-aux f before-list FROM))))