From 70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
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.
---
 isar/isabelle-system.el |  5 +++--
 isar/isar-autotest.el   | 10 +++++-----
 isar/isar-profiling.el  |  2 +-
 3 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'isar')

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