diff options
| -rw-r--r-- | generic/proof-menu.el | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 9b95a9b5..18b4126e 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -458,13 +458,13 @@ If in three window or multiple frame mode, display two buffers." This is intended for defining proof assistant specific functions. STRING is inserted using `proof-insert', which see. KEY is added onto proof-assistant map." - (if key - (eval ;; eval-after-load "proof" ? - `(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))) - `(defun ,fn () - ,(concat "Shortcut command to insert " string " into the current buffer.") - (interactive) - (proof-insert ,string))) + `(progn + (if ,key + (define-key (proof-ass keymap) (quote ,key) (quote ,fn))) + (defun ,fn () + ,(concat "Shortcut command to insert " string " into the current buffer.") + (interactive) + (proof-insert ,string)))) ;;;###autoload (defmacro proof-definvisible (fn string &optional key) @@ -472,13 +472,13 @@ KEY is added onto proof-assistant map." This is intended for defining proof assistant specific functions. STRING is sent using proof-shell-invisible-command, which see. KEY is added onto proof-assistant map." - (if key - (eval ;; eval-after-load "proof" ? - `(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))) - `(defun ,fn () - ,(concat "Command to send " string " to the proof assistant.") - (interactive) - (proof-shell-invisible-command ,string))) + `(progn + (if ,key + (define-key (proof-ass keymap) (quote ,key) (quote ,fn))) + (defun ,fn () + ,(concat "Command to send " string " to the proof assistant.") + (interactive) + (proof-shell-invisible-command ,string)))) (defun proof-def-favourite (command inscript menuname &optional key new) "Define and a \"favourite\" proof assisant function. |