diff options
| -rw-r--r-- | coq/coq-abbrev.el | 2 | ||||
| -rw-r--r-- | coq/coq-autotest.el | 2 | ||||
| -rw-r--r-- | isar/isar-autotest.el | 2 | ||||
| -rw-r--r-- | lib/proof-compat.el | 34 |
4 files changed, 3 insertions, 37 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index e79f361f..31ee58d6 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -54,7 +54,7 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(eval-when (load) +(unless (noninteractive) (if (and (boundp 'coq-mode-abbrev-table) (not (equal coq-mode-abbrev-table (make-abbrev-table)))) (message "Coq abbrevs already exists, default not loaded") diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 0e12d48c..160efdcb 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -8,7 +8,7 @@ (require 'pg-autotest) ;; The included test files -(eval-when (load) +(unless (noninteractive) (pg-autotest message "Testing standard examples") (pg-autotest script-wholefile "coq/example.v") (pg-autotest script-wholefile "coq/example-x-symbol.v") diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 2d5beef5..6bcfc0bc 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -7,7 +7,7 @@ (require 'pg-autotest) -(eval-when (load) +(unless (noninteractive) ;; The included test files (pg-autotest message "Testing standard Example.thy, Example-Xsym.thy") diff --git a/lib/proof-compat.el b/lib/proof-compat.el index 1f8e205a..96a73ff3 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -694,40 +694,6 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged." (not (valid-specifier-tag-p 'mule-fonts))) (define-specifier-tag 'mule-fonts)) -;; -;; Useful eval-when macro from cl-macs in XEmacs -;; - -(unless (fboundp 'eval-when) - (defmacro eval-when (when &rest body) - "(eval-when (WHEN...) BODY...): control when BODY is evaluated. -If `compile' is in WHEN, BODY is evaluated when compiled at top-level. -If `load' is in WHEN, BODY is evaluated when loaded after top-level compile. -If `eval' is in WHEN, BODY is evaluated when interpreted or at non-top-level." - (if (and (fboundp 'cl-compiling-file) (cl-compiling-file) - (not cl-not-toplevel) (not (boundp 'for-effect))) ; horrible kludge - (let ((comp (or (memq 'compile when) (memq :compile-toplevel when))) - (cl-not-toplevel t)) - (if (or (memq 'load when) (memq :load-toplevel when)) - (if comp (cons 'progn (mapcar 'cl-compile-time-too body)) - (list* 'if nil nil body)) - (progn (if comp (eval (cons 'progn body))) nil))) - (and (or (memq 'eval when) (memq :execute when)) - (cons 'progn body)))) - -(defun cl-compile-time-too (form) - (or (and (symbolp (car-safe form)) (get (car-safe form) 'byte-hunk-handler)) - (setq form (macroexpand - form (cons '(eval-when) byte-compile-macro-environment)))) - (cond ((eq (car-safe form) 'progn) - (cons 'progn (mapcar 'cl-compile-time-too (cdr form)))) - ((eq (car-safe form) 'eval-when) - (let ((when (nth 1 form))) - (if (or (memq 'eval when) (memq :execute when)) - (list* 'eval-when (cons 'compile when) (cddr form)) - form))) - (t (eval form) form)))) - ;; End of proof-compat.el (provide 'proof-compat) |