From 70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 26 Feb 2017 00:28:18 -0500 Subject: Fix incorrect assumption that noninteractive == byte-compiling The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. --- coq/coq-abbrev.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'coq/coq-abbrev.el') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 2b318dea..a05c9853 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)) ;;;;; -- cgit v1.2.3 From d3170a0cbe470cd620bc16e04eb148e554047d35 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 20:15:09 -0500 Subject: Remove uses of defpgdefault in coq-abbrev This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'. --- coq/coq-abbrev.el | 10 ++++------ generic/pg-pamacs.el | 2 ++ 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'coq/coq-abbrev.el') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index a05c9853..30ec60c4 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -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 @@ -300,7 +300,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 `( "" @@ -338,12 +338,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/generic/pg-pamacs.el b/generic/pg-pamacs.el index 8b9b83c7..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 -- cgit v1.2.3