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 +- coq/coq-autotest.el | 2 +- generic/pg-user.el | 4 ++-- generic/proof-splash.el | 2 +- generic/proof-useropts.el | 1 + generic/proof.el | 2 +- hol-light/hol-light-autotest.el | 4 ++-- isar/isabelle-system.el | 5 +++-- isar/isar-autotest.el | 10 +++++----- isar/isar-profiling.el | 2 +- 10 files changed, 18 insertions(+), 16 deletions(-) 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)) ;;;;; diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index b6b361ed..a8367b5c 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -16,7 +16,7 @@ (defvar coq-compile-before-require nil)) -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start 'debug) 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-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 diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el index 20c16727..b9924c41 100644 --- a/hol-light/hol-light-autotest.el +++ b/hol-light/hol-light-autotest.el @@ -8,14 +8,14 @@ (eval-when-compile (require 'cl)) -(eval-when (compile) +(eval-when-compile (require 'proof-site) (proof-ready-for-assistant 'coq) (defvar coq-compile-before-require nil)) (require 'pg-autotest) -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start 'debug) (pg-autotest log ".autotest.log") ; convention diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index 5352043d..64cd768f 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -73,6 +73,7 @@ unverified. Otherwise, returns non-nil if isa-isabelle-command is surely an executable with full path." (interactive "p") (when (and (not noninteractive) + (not (bound-and-true-p byte-compile-current-file)) (not proof-rsh-command) (or force isabelle-not-found @@ -139,7 +140,7 @@ generated with the Lisp form `(isa-tool-list-logics)'." :type (list 'string) :group 'isabelle) -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (setq isabelle-logics-available (isa-tool-list-logics))) (defcustom isabelle-chosen-logic nil @@ -287,7 +288,7 @@ for you, you should disable this behaviour." :help (format "Switch to %s logic" l))) isabelle-logics-available))))) -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (isabelle-logics-menu-calculate)) (defvar isabelle-time-to-refresh-logics t diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 60fa2ebc..10ce61a1 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -20,7 +20,7 @@ (declare-function isar-tracing:auto-solve-direct-toggle "isar.el") (declare-function isar-proof:parallel-proofs-toggle "isar.el") -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start) ; can add 'debug flag for debug-on-error @@ -89,10 +89,10 @@ (pg-autotest script-randomjumps "isar/Example.thy" 8) (when isar-long-tests - (pg-autotest remark "Larger files...") - (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest script-wholefile "isar/ex/Tarski.thy") - (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test? + (pg-autotest remark "Larger files...") + (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") + (pg-autotest script-wholefile "isar/ex/Tarski.thy") + (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test? (pg-autotest remark "Testing restarting the prover") diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 8984f1b0..101d04ee 100644 --- a/isar/isar-profiling.el +++ b/isar/isar-profiling.el @@ -19,7 +19,7 @@ (require 'pg-autotest) (require 'pg-dev) -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest log ".profile.log") ; convention -- cgit v1.2.3