From 7eb2222e64e25f1bd224fa5a04aba3982da0f5d4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 13 Jun 2004 21:10:16 +0000
Subject: Generalise proof-def-invisible.

---
 generic/proof-menu.el | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 4d879c35..c9a99f83 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -534,16 +534,22 @@ KEY is added onto proof-assistant map."
   "Define function FN to send STRING to proof assistant, optional keydef KEY.
 This is intended for defining proof assistant specific functions.
 STRING is sent using proof-shell-invisible-command, which see.
+STRING may be a string or a function which returns a string.
 KEY is added onto proof-assistant map."
   `(progn
      (if ,key
 	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
      (defun ,fn ()
        ,(concat "Command to send " 
-		(replace-in-string  string "\\\\" "\\\\=") ;; for substitute-command-keys
+		(if (stringp string)
+		    (replace-in-string  
+		     string "\\\\" "\\\\=") ;; for substitute-command-keys
+		  "an instruction")
 		" to the proof assistant.")
        (interactive)
-       (proof-shell-invisible-command ,string))))
+       ,(if (stringp string)
+	    (list 'proof-shell-invisible-command string)
+	  (list 'proof-shell-invisible-command (eval string))))))
 
 (defun proof-def-favourite (command inscript menuname &optional key new)
   "Define and a \"favourite\" proof assisant function.
-- 
cgit v1.2.3