Merge pull request #157 from ProofGeneral/elpa

[WIP] ELPA/MELPA support

10 files changed, 57 insertions, 75 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 062f7580..79231ad9 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -71,7 +71,7 @@
     ;; DA: how about above, just temporarily disable saving?
     (message "Coq default abbrevs loaded")))
 
-(unless noninteractive
+(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
   (coq-install-abbrevs))
 ;;;;;
 
@@ -98,7 +98,7 @@ It was constructed with `proof-defstringset-fn'.")
 
 ;; The coq menu partly built from tables
 
-;; Common part (scrit, response and goals buffers)
+;; Common part (script, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
     ["Toggle 3 Windows Mode" proof-three-window-toggle
@@ -304,7 +304,7 @@ It was constructed with `proof-defstringset-fn'.")
     ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"]
     ))
 
-(defpgdefault menu-entries
+(setq-default coq-menu-entries
   (append coq-menu-common-entries
   `(
     ""
@@ -342,12 +342,10 @@ It was constructed with `proof-defstringset-fn'.")
      ["help" coq-local-vars-list-show-doc t]
      ["Compile" coq-Compile t]))))
 
-(defpgdefault help-menu-entries
+(setq-default coq-help-menu-entries
   '(["help on setting prog name persistently for a file" 
      coq-local-vars-list-show-doc t]))
 
-(defpgdefault other-buffers-menu-entries coq-menu-common-entries)
-
-
+(setq-default coq-other-buffers-menu-entries coq-menu-common-entries)
 
 (provide 'coq-abbrev)
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index b6b361ed..e3c4b978 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -10,13 +10,10 @@
 
 (require 'pg-autotest)
 
-(eval-when (compile)
-  (require 'proof-site)
-  (proof-ready-for-assistant 'coq)
-  (defvar coq-compile-before-require nil))
+(require 'proof-site)
+(defvar coq-compile-before-require)
 
-
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
 
   (pg-autotest start 'debug)
 
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 72a16881..f6adc5cd 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -15,14 +15,12 @@
 
 (require 'proof-shell)
 (require 'coq-system)
+(require 'compile)
 
 (eval-when (compile)
   ;;(defvar coq-pre-v85 nil)
-  (require 'compile)
-  (defvar coq-confirm-external-compilation nil); defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
-  (proof-ready-for-assistant 'coq))     ; compile for coq
-
+  (defvar coq-confirm-external-compilation); defpacustom
+  (defvar coq-compile-parallel-in-background)) ; defpacustom
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -34,7 +32,7 @@
 ;; coq-par-compile, respectively. However, the :initialization
 ;; function of a defcustom seems to be evaluated when reading the
 ;; defcustom form. Therefore, these functions must be defined already,
-;; when the defpacustum coq-compile-parallel-in-background is read.
+;; when the defcustom coq-compile-parallel-in-background is read.
 
 (defun coq-par-enable ()
   "Enable parallel compilation.
@@ -157,7 +155,7 @@ Ignore any quick setting for Coq versions before 8.5."
   :group 'coq
   :package-version '(ProofGeneral . "4.1"))
 
-(defpacustom compile-before-require nil
+(defcustom coq-compile-before-require nil
   "If non-nil, check dependencies of required modules and compile if necessary.
 If non-nil ProofGeneral intercepts \"Require\" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
@@ -169,7 +167,9 @@ This option can be set/reset via menu
   :safe 'booleanp
   :group 'coq-auto-compile)
 
-(defpacustom compile-parallel-in-background nil
+(proof-deftoggle coq-compile-before-require)
+
+(defcustom coq-compile-parallel-in-background nil
   "Choose the internal compilation method.
 When Proof General compiles itself, you have the choice between
 two implementations. If this setting is nil, then Proof General
@@ -184,8 +184,12 @@ This option can be set/reset via menu
 `Coq -> Auto Compilation -> Compile Parallel In Background'."
   :type 'boolean
   :safe 'booleanp
-  :group 'coq-auto-compile
-  :eval (coq-switch-compilation-method))
+  :group 'coq-auto-compile)
+
+(proof-deftoggle coq-compile-parallel-in-background)
+
+(defun coq-compile-parallel-in-background ()
+  (coq-switch-compilation-method))
 
 ;; defpacustom fails to call :eval during inititialization, see trac #456
 (coq-switch-compilation-method)
@@ -407,7 +411,7 @@ This option can be set via menu
 ;; define coq-lock-ancestors-toggle
 (proof-deftoggle coq-lock-ancestors)
 
-(defpacustom confirm-external-compilation t
+(defcustom coq-confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index e5179390..878fb895 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -22,7 +22,7 @@
 ;     (message "%.06f" (float-time (time-since time)))))
 
 (eval-when-compile
-  (defvar coq-script-indent nil))
+  (defvar coq-script-indent))
 
 (defconst coq-any-command-regexp
   (proof-regexp-alt-list coq-keywords))
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 846371b4..cd29e218 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -15,8 +15,8 @@
   (require 'cl))
 
 (eval-when (compile)
-  (defvar coq-prog-name nil)
-  (defvar coq-load-path nil))
+  (defvar coq-prog-name)
+  (defvar coq-load-path))
 
 
 ;;; Code:
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index f9b317c2..05703e45 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -28,10 +28,7 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems))       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index a1b2d30a..ee4181ae 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -19,10 +19,7 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil)       ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems))       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e97d268c..156d39e1 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -9,14 +9,9 @@
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
 (require 'coq-db)
+(require 'span)
 
-(eval-when-compile
-  (require 'span)
-  (defvar coq-goal-command-regexp nil)
-  (defvar coq-save-command-regexp-strict nil))
-
-
- ;;; keyword databases
+;;; keyword databases
 
 (defcustom coq-user-tactics-db nil
   "User defined tactic information.  See `coq-syntax-db' for
diff --git a/coq/coq-system.el b/coq/coq-system.el
index aad7d386..ad85a960 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -16,12 +16,11 @@
 
 (eval-when-compile
   (require 'cl)
-  (require 'proof-compat)
-  (proof-ready-for-assistant 'coq))
+  (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar coq-prog-args nil)
-  (defvar coq-debug nil))
+  (defvar coq-prog-args)
+  (defvar coq-debug))
 
 (defcustom coq-prog-env nil
   "List of environment settings d to pass to Coq process.
diff --git a/coq/coq.el b/coq/coq.el
index 418fbb4c..43fd49f6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -19,19 +19,18 @@
   (require 'newcomment)
   (require 'etags)
   (unless (proof-try-require 'smie)
-    (defvar smie-indent-basic nil)
-    (defvar smie-rules-function nil))
-  (defvar proof-info nil)       ; dynamic scope in proof-tree-urgent-action
-  (defvar action nil)       ; dynamic scope in coq-insert-as stuff
-  (defvar string nil)       ; dynamic scope in coq-insert-as stuff
-  (defvar old-proof-marker nil)
-                         ; dynamic scoq in coq-proof-tree-enable-evar-callback
-  (defvar coq-auto-insert-as nil)    ; defpacustom
-  (defvar coq-time-commands nil)        ; defpacustom
+    (defvar smie-indent-basic)
+    (defvar smie-rules-function))
+  (defvar proof-info)       ; dynamic scope in proof-tree-urgent-action
+  (defvar action)       ; dynamic scope in coq-insert-as stuff
+  (defvar string)       ; dynamic scope in coq-insert-as stuff
+  (defvar old-proof-marker)
+                                        ; dynamic scoq in coq-proof-tree-enable-evar-callback
+  (defvar coq-auto-insert-as)    ; defpacustom
+  (defvar coq-time-commands)        ; defpacustom
   (defvar coq-use-project-file t)        ; defpacustom
-  (defvar coq-use-editing-holes nil)    ; defpacustom
-  (defvar coq-hide-additional-subgoals nil) ; defpacustom
-  (proof-ready-for-assistant 'coq))     ; compile for coq
+  (defvar coq-use-editing-holes)    ; defpacustom
+  (defvar coq-hide-additional-subgoals))
 
 (require 'proof)
 (require 'coq-system)                   ; load path, option, project file etc.
@@ -306,27 +305,23 @@ See also `coq-hide-additional-subgoals'."
 ;; Derived modes
 ;;
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-shell-mode proof-shell-mode
-    "Coq Shell" nil
-    (coq-shell-mode-config)))
+(define-derived-mode coq-shell-mode proof-shell-mode
+  "Coq Shell" nil
+  (coq-shell-mode-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-response-mode proof-response-mode
+(define-derived-mode coq-response-mode proof-response-mode
   "Coq Response" nil
-    (coq-response-config)))
+  (coq-response-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-mode proof-mode "Coq"
-    "Major mode for Coq scripts.
+(define-derived-mode coq-mode proof-mode "Coq"
+  "Major mode for Coq scripts.
 
 \\{coq-mode-map}"
-    (coq-mode-config)))
+  (coq-mode-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-goals-mode proof-goals-mode
-    "Coq Goals" nil
-    (coq-goals-mode-config)))
+(define-derived-mode coq-goals-mode proof-goals-mode
+  "Coq Goals" nil
+  (coq-goals-mode-config))
 
 ;; Indentation and navigation support via SMIE.
 
@@ -1199,7 +1194,7 @@ flag Printing All set."
 
 ;; Check
 (eval-when (compile)
-  (defvar coq-auto-adapt-printing-width nil)); defpacustom
+  (defvar coq-auto-adapt-printing-width)); defpacustom
 
 ;; Since Printing Width is a synchronized option in coq (?) it is retored
 ;; silently to a previous value when retracting. So we reset the stored width
@@ -1210,7 +1205,7 @@ flag Printing All set."
 ;; we can remove this.
 (defun coq-set-auto-adapt-printing-width (&optional symb val); args are for :set compatibility
   "Function called when setting `auto-adapt-printing-width'"
-  (setq symb val)
+  (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes)
   (if coq-auto-adapt-printing-width
       (progn
         (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)