Added proof-assistant-keymap and commands for defining insert keys.

1 files changed, 19 insertions, 3 deletions

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."