diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-02-25 19:55:51 -0500 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-03-08 15:06:17 -0500 |
commit | c1f6c9c2f87edea03d9c279719f0f4a10c396db0 (patch) | |
tree | cb55f1e0fa7c086a53e75929b4fdcfaa2d7b89b0 | |
parent | 031a5780575f3b87124df303b42e202aa5e1c418 (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.el | 18 | ||||
-rw-r--r-- | coq/coq-par-compile.el | 5 | ||||
-rw-r--r-- | coq/coq-seq-compile.el | 5 |
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) |