Merge pull request #157 from ProofGeneral/elpa

[WIP] ELPA/MELPA support

4 files changed, 24 insertions, 30 deletions

diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 5352043d..d4ef3762 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -16,13 +16,12 @@
   (require 'cl))			;  mapcan, eval-when
 
 (eval-when (compile)
-  (require 'span)		        
-  (require 'scomint)		        
+  (require 'span)
+  (require 'scomint)
   (require 'proof-site)
   (require 'proof-menu)
   (require 'proof-syntax)
-  (proof-ready-for-assistant 'isar)	; compile for isar
-  (defvar proof-assistant-menu nil))
+  (defvar proof-assistant-menu))
 
 (declare-function mapcan "cl-extra")	; spurious bytecomp warning
 
@@ -73,6 +72,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 +139,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 +287,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..091d2a0a 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -11,16 +11,16 @@
 (require 'pg-autotest)
 
 (eval-when (compile)
-  (require 'cl)
-  (require 'proof-site)
-  (proof-ready-for-assistant 'isar))
+  (require 'cl))
 
+(require 'proof-site)
+(proof-ready-for-assistant 'isar)
 
 (declare-function isar-tracing:auto-quickcheck-toggle "isar.el")
 (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..0cf19348 100644
--- a/isar/isar-profiling.el
+++ b/isar/isar-profiling.el
@@ -8,9 +8,8 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
-  (require 'proof-site)
-  (proof-ready-for-assistant 'isar))  
+(require 'proof-site)
+(proof-ready-for-assistant 'isar)
 
 (declare-function isar-tracing:auto-solve-toggle "isar.el")
 (declare-function isar-tracing:auto-quickcheck-toggle "isar.el")
@@ -19,7 +18,7 @@
 (require 'pg-autotest)
 (require 'pg-dev)
 
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
 
   (pg-autotest log ".profile.log")  ; convention
 
diff --git a/isar/isar.el b/isar/isar.el
index bc28d34d..b8119ee6 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -25,10 +25,9 @@
   (require 'pg-goals)
   (require 'pg-vars)
   (require 'outline)
-  (defvar comment-quote-nested nil)
-  (defvar isar-use-find-theorems-form nil)
-  (defvar isar-use-linear-undo nil)
-  (proof-ready-for-assistant 'isar))	; compile for isar
+  (defvar comment-quote-nested)
+  (defvar isar-use-find-theorems-form)
+  (defvar isar-use-linear-undo))
 
 (require 'proof)
 (require 'isabelle-system)		; system code
@@ -303,28 +302,24 @@ This is called when Proof General spots output matching
 ;;
 ;; use eval-and-compile to define vars for byte comp.
 
-(eval-and-compile
 (define-derived-mode isar-shell-mode proof-shell-mode
    "Isabelle Shell" nil
-   (isar-shell-mode-config)))
+   (isar-shell-mode-config))
 
-(eval-and-compile
 (define-derived-mode isar-response-mode proof-response-mode
   "Isar Messages" nil
-  (isar-response-mode-config)))
+  (isar-response-mode-config))
 
-(eval-and-compile
 (define-derived-mode isar-goals-mode proof-goals-mode
   "Isar Proofstate" nil
-  (isar-goals-mode-config)))
+  (isar-goals-mode-config))
 
-(eval-and-compile
 (define-derived-mode isar-mode proof-mode
   "Isar"
   "Major mode for editing Isar proof scripts.
 
 \\{isar-mode-map}"
-  (isar-mode-config)))
+  (isar-mode-config))