Merge pull request #157 from ProofGeneral/elpa

[WIP] ELPA/MELPA support

10 files changed, 33 insertions, 60 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 6a27cd29..a8a52099 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -16,13 +16,12 @@
 
 (require 'proof-utils)
 
-(eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time
-  (define-derived-mode proof-universal-keys-only-mode fundamental-mode
-    proof-general-name "Universal keymaps only"
-    ;; Doesn't seem to supress TAB, RET
-    (suppress-keymap proof-universal-keys-only-mode-map 'all)
-    (proof-define-keys proof-universal-keys-only-mode-map
-		       proof-universal-keys)))
+(define-derived-mode proof-universal-keys-only-mode fundamental-mode
+  proof-general-name "Universal keymaps only"
+  ;; Doesn't seem to supress TAB, RET
+  (suppress-keymap proof-universal-keys-only-mode-map 'all)
+  (proof-define-keys proof-universal-keys-only-mode-map
+                     proof-universal-keys))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 4958b360..d7bb1bf3 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -155,6 +155,8 @@ Usage: (defpgdefault SYM VALUE)"
 ;;;###autoload
 (defun proof-defpacustom-fn (name val args)
   "As for macro `defpacustom' but evaluating arguments."
+  (unless (and proof-assistant (not (string= proof-assistant "")))
+    (error "No proof assistant defined"))
   (let (newargs setting evalform type descr)
     (while args
       (cond
@@ -257,10 +259,6 @@ Additional properties in the ARGS prop list may include:
 		     askprefs message.
 
 This macro also extends the `proof-assistant-settings' list."
-  (eval-when-compile
-    (if (boundp 'proof-assistant-symbol)
-	;; declare variable to compiler to prevent warnings
-	(eval `(defvar ,(proof-ass-sym name) nil "Dummy for compilation."))))
   `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))
 
 
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 893d1f6f..8b6a413a 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -99,33 +99,21 @@ Internal variable, setting this will have no effect!")
   "List of GNU Emacs frame parameters for secondary frames.")
 
 (defun proof-multiple-frames-enable ()
-  ; special-display-regexps is obsolete, let us let it for a while and
-  ; remove it later
-  (unless (eval-when-compile (boundp 'display-buffer-alist))
-    (let ((spdres (cons
-		   pg-response-special-display-regexp
-		   proof-multiframe-parameters)))
-      (if proof-multiple-frames-enable
-	  (add-to-list 'special-display-regexps spdres)
-	(setq special-display-regexps
-	      (delete spdres special-display-regexps)))))
-  ; This is the current way to do it
-  (when (eval-when-compile (boundp 'display-buffer-alist))
-    (let
-	((display-buffer-entry
-	  (cons pg-response-special-display-regexp
-	    `((display-buffer-reuse-window display-buffer-pop-up-frame) .
-	      ((reusable-frames . t)
-	       (pop-up-frame-parameters
-		.
-		,proof-multiframe-parameters))))))
-      (if proof-multiple-frames-enable
-	  (add-to-list
-	   'display-buffer-alist
-	   display-buffer-entry)
-	;(add-to-list 'display-buffer-alist (proof-buffer-dislay))
-	(setq display-buffer-alist
-	      (delete display-buffer-entry display-buffer-alist)))))
+  (let
+      ((display-buffer-entry
+        (cons pg-response-special-display-regexp
+          `((display-buffer-reuse-window display-buffer-pop-up-frame) .
+            ((reusable-frames . t)
+             (pop-up-frame-parameters
+              .
+              ,proof-multiframe-parameters))))))
+    (if proof-multiple-frames-enable
+        (add-to-list
+         'display-buffer-alist
+         display-buffer-entry)
+      ;(add-to-list 'display-buffer-alist (proof-buffer-dislay))
+      (setq display-buffer-alist
+            (delete display-buffer-entry display-buffer-alist))))
   (proof-layout-windows))
 
 (defun proof-three-window-enable ()
@@ -521,9 +509,7 @@ and start at the first error."
 			  ;; Pop up a window.
 			  (display-buffer
                            proof-response-buffer
-                           (and (eval-when-compile
-                                  (boundp 'display-buffer-alist))
-                                proof-multiple-frames-enable
+                           (and proof-multiple-frames-enable
                                 (cons nil proof-multiframe-parameters))))))
 		  ;; Make sure the response buffer stays where it is,
 		  ;; and make sure source buffer is visible
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 513b477b..effe1eb5 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -563,9 +563,9 @@ last use time, to discourage saving these into the users database."
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless noninteractive ; during compilation
+(unless (bound-and-true-p byte-compile-current-file)
   (eval-after-load "completion"
-  '(proof-add-completions)))
+    '(proof-add-completions)))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to proof-case-fold-search."
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index df617347..f029afcb 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -10,23 +10,13 @@
 (require 'cl)				; mapcan
 
 ;;; Code:
-(eval-when (compile)
-  (defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific
-  (defvar proof-mode-map nil))
-
-(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
-(require 'proof-useropts)
-(require 'proof-config)
-
-
-    
-
-
 (eval-when-compile
   (defvar proof-assistant-menu)	  ; defined by macro in proof-menu-define-specific
   (defvar proof-mode-map))
-    
 
+(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
+(require 'proof-useropts)
+(require 'proof-config)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4547a835..f79b78c2 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1912,7 +1912,6 @@ Error messages are displayed as usual."
 ;; Proof General shell mode definition
 ;;
 
-;(eval-and-compile			; to define vars
 ;;;###autoload
 (define-derived-mode proof-shell-mode scomint-mode
   "proof-shell" "Proof General shell mode class for proof assistant processes"
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 671c3c82..17ca325c 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -163,7 +163,7 @@ You can use customize to set this variable."
 (require 'proof-autoloads)
 
 (eval-when-compile
-  (defvar Info-dir-contents nil))
+  (defvar Info-dir-contents))
 
 ;; Add the info directory to the Info path
 (if (file-exists-p proof-info-directory) ; for safety
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 25db0946..7e7b8d54 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -264,7 +264,7 @@ binding to remove this buffer."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen noninteractive)
+  (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
     (if proof-splash-enable
 	(progn
 	  ;; disable ordinary emacs splash
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index b2cbb97a..eb9942a7 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -43,6 +43,7 @@ approximation we test whether proof-config is fully-loaded yet."
   (set-default sym value)
   (when (and
 	 (not noninteractive)
+	 (not (bound-and-true-p byte-compile-current-file))
 	 (featurep 'pg-custom)
 	 (featurep 'proof-config))
       (if (fboundp sym)
diff --git a/generic/proof.el b/generic/proof.el
index 1acfae71..4e7ddbea 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -26,7 +26,7 @@
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 
-(unless noninteractive
+(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
   (proof-splash-message))		; welcome the user now.
 
 (require 'proof-compat)			; Emacs and OS compatibility