aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2017-02-25 19:55:51 -0500
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2017-03-08 15:06:17 -0500
commitc1f6c9c2f87edea03d9c279719f0f4a10c396db0 (patch)
treecb55f1e0fa7c086a53e75929b4fdcfaa2d7b89b0
parent031a5780575f3b87124df303b42e202aa5e1c418 (diff)
Remove uses of defpacustom in coq-compile-common
This file is `require'-d from other places, at compile time. This doesn't work nicely with compilation by package.el (PG complains and says "defpacustom: Proof assistant setting compile-before-require re-defined!")
-rw-r--r--coq/coq-compile-common.el18
-rw-r--r--coq/coq-par-compile.el5
-rw-r--r--coq/coq-seq-compile.el5
3 files changed, 14 insertions, 14 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index c557f474..f6adc5cd 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -32,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.
@@ -155,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
@@ -167,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
@@ -182,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)
@@ -405,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-par-compile.el b/coq/coq-par-compile.el
index fbe38a1e..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) ; dynamic scope in p-s-extend-queue-hook
- (defvar coq-compile-before-require) ; defpacustom
- (defvar coq-compile-parallel-in-background) ; defpacustom
- (defvar coq-confirm-external-compilation)); 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 5ecfbf4b..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) ; dynamic scope in p-s-extend-queue-hook
- (defvar coq-compile-before-require) ; defpacustom
- (defvar coq-compile-parallel-in-background) ; defpacustom
- (defvar coq-confirm-external-compilation)); defpacustom
+ (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook
(require 'coq-compile-common)