From e6d5b8b8b19ae60f76f34563b0a8eca4fb89e6e2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 2 May 2000 12:05:41 +0000 Subject: Added proof-assistant-keymap and commands for defining insert keys. --- generic/proof.el | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) (limited to 'generic/proof.el') diff --git a/generic/proof.el b/generic/proof.el index ab51aa1e..102a8727 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -196,16 +196,32 @@ It was constructed with the macro proof-customize-toggle.") ;; FIXME: combine this with above, and remove messing calls in ;; proof-script. -;; FIXME: rather broken wrt to ARG. (defmacro proof-deftoggle (var) - "Define a function VAR-toggle to be a toggler for variable VAR. -See proof-customize-toggle." + "Define a function VAR-toggle for toggling a boolean customize setting VAR. +The toggle function uses customize-set-variable to change the variable." `(defun ,(intern (concat (symbol-name var) "-toggle")) (arg) + ,(concat "Toggle " (symbol-name var) ". With ARG, turn on iff ARG>0. +This function simply uses customize-set-variable to set the variable. +It was constructed with the macro proof-deftoggle.") (interactive "P") (customize-set-variable (quote ,var) (if (null arg) (not ,var) (> (prefix-numeric-value arg) 0))))) + +(defmacro proof-defshortcut (fn string &optional key) + "Define shortcut function FN to insert STRING, optional keydef KEY. +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 + `(define-key proof-assistant-keymap ,key (quote ,fn)))) + `(defun ,fn () + "Shortcut command to insert a string." + (interactive) + (proof-insert ,string))) + (defun proof-try-require (symbol) "Try requiring SYMBOL. No error if the file for SYMBOL isn't found." -- cgit v1.2.3