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.

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