diff options
| -rw-r--r-- | coq/coq.el | 26 | ||||
| -rw-r--r-- | generic/pg-assoc.el | 13 | ||||
| -rw-r--r-- | generic/proof-shell.el | 1 | ||||
| -rw-r--r-- | isar/isar.el | 12 | ||||
| -rw-r--r-- | lib/pg-fontsets.el | 3 |
5 files changed, 22 insertions, 33 deletions
@@ -306,27 +306,23 @@ See also `coq-hide-additional-subgoals'." ;; Derived modes ;; -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-shell-mode proof-shell-mode - "Coq Shell" nil - (coq-shell-mode-config))) +(define-derived-mode coq-shell-mode proof-shell-mode + "Coq Shell" nil + (coq-shell-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-response-mode proof-response-mode +(define-derived-mode coq-response-mode proof-response-mode "Coq Response" nil - (coq-response-config))) + (coq-response-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-mode proof-mode "Coq" - "Major mode for Coq scripts. +(define-derived-mode coq-mode proof-mode "Coq" + "Major mode for Coq scripts. \\{coq-mode-map}" - (coq-mode-config))) + (coq-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-goals-mode proof-goals-mode - "Coq Goals" nil - (coq-goals-mode-config))) +(define-derived-mode coq-goals-mode proof-goals-mode + "Coq Goals" nil + (coq-goals-mode-config)) ;; Indentation and navigation support via SMIE. diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index 6a27cd29..a8a52099 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -16,13 +16,12 @@ (require 'proof-utils) -(eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time - (define-derived-mode proof-universal-keys-only-mode fundamental-mode - proof-general-name "Universal keymaps only" - ;; Doesn't seem to supress TAB, RET - (suppress-keymap proof-universal-keys-only-mode-map 'all) - (proof-define-keys proof-universal-keys-only-mode-map - proof-universal-keys))) +(define-derived-mode proof-universal-keys-only-mode fundamental-mode + proof-general-name "Universal keymaps only" + ;; Doesn't seem to supress TAB, RET + (suppress-keymap proof-universal-keys-only-mode-map 'all) + (proof-define-keys proof-universal-keys-only-mode-map + proof-universal-keys)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 51305eef..93f1bbef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1911,7 +1911,6 @@ Error messages are displayed as usual." ;; Proof General shell mode definition ;; -;(eval-and-compile ; to define vars ;;;###autoload (define-derived-mode proof-shell-mode scomint-mode "proof-shell" "Proof General shell mode class for proof assistant processes" diff --git a/isar/isar.el b/isar/isar.el index bc28d34d..556a4973 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -303,28 +303,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)) diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el index 2c0528cc..c4d76efc 100644 --- a/lib/pg-fontsets.el +++ b/lib/pg-fontsets.el @@ -21,8 +21,7 @@ ;;; Code: -(eval-and-compile - (require 'fontset)) ; needed for some emacsen without X +(require 'fontset) (defcustom pg-fontsets-default-fontset nil "*Name of default fontset to use with Proof General." |