Added menu binding for finding theorems.

Added extra doc strings to hair macro definitions of functions.

1 files changed, 28 insertions, 11 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index e71f8e77..72fafb34 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1445,24 +1445,24 @@ even more dangerous than proof-try-command."
      (error "Proof General not configured for this: set %s" 
 	    ,(symbol-name var))))
 
-(defmacro proof-define-assistant-command (fn cmdvar)
+(defmacro proof-define-assistant-command (fn doc cmdvar)
   "Define command FN to send string CMDVAR to proof assistant."
   `(defun ,fn ()
-     ,(concat "Issue a command to the assistant from " 
+     ,(concat doc "\nIssues a command to the assistant from " 
 	      (symbol-name cmdvar) ".")
      (interactive)
      (proof-if-setting-configured ,cmdvar
        (proof-shell-invisible-command
 	(concat ,cmdvar proof-terminal-string)))))
 
-(defmacro proof-define-assistant-command-witharg (fn cmdvar prompt &rest body)
+(defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)
   "Define command FN to prompt for string CMDVAR to proof assistant.
 CMDVAR is a function or string.  Automatically has history."
   `(progn
      (defvar ,(intern (concat (symbol-name fn) "-history")) nil
        ,(concat "History of arguments for " (symbol-name fn) "."))
      (defun ,fn (arg)
-     ,(concat "Issue a command based on ARG to the assistant, using " 
+     ,(concat doc "\nIssues a command based on ARG to the assistant, using " 
 	      (symbol-name cmdvar) ".\n"
 	      "The user is prompted for an argument.")
       (interactive
@@ -1498,26 +1498,36 @@ Start up the proof assistant if necessary."
 ;; Commands which do not require a prompt and send an invisible command.
 ;;
 
-(proof-define-assistant-command proof-ctxt proof-ctxt-string)
-(proof-define-assistant-command proof-help proof-help-string)
-(proof-define-assistant-command proof-prf  proof-prf-string)
+(proof-define-assistant-command proof-prf  
+  "Show the current proof state."
+  proof-prf-string)
+(proof-define-assistant-command proof-ctxt 
+  "Show the current context."
+  proof-ctxt-string)
+(proof-define-assistant-command proof-help 
+  "Show a help or information message from the proof assistant.
+Typically, a list of syntax of commands available."
+  proof-help-string)
 
 ;;
 ;; Commands which require an argument, and maybe affect the script.
 ;;
 
 (proof-define-assistant-command-witharg proof-find-theorems
+ "Search for items containing a given constant."					
  proof-find-theorems-command
  "Find theorems containing the constant"
  (proof-shell-invisible-command arg))
 
 (proof-define-assistant-command-witharg proof-issue-goal
+ "Write a goal command in the script, prompting for the goal."
  proof-goal-command
  "Goal"
  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
    (proof-issue-new-command arg)))
 
 (proof-define-assistant-command-witharg proof-issue-save 
+ "Write a save/qed command in the script, prompting for the theorem name."
  proof-save-command
  "Save as"
  (let ((proof-one-command-per-line t))   ; Saves always start at a new line
@@ -1570,14 +1580,19 @@ No action if BUF is nil."
   "Proof General buffer menu.")
 
 ;; FIXME da: could move this elsewhere.  
+;; FIXME da: rationalize toolbar menu items with this menu, i.e.
+;; remove common stuff.
 (defvar proof-shared-menu
   (append
     (list
+     ["Display proof state"
+      proof-prf
+      :active (proof-shell-live-buffer)]
      ["Display context"
       proof-ctxt
       :active (proof-shell-live-buffer)]
-     ["Display proof state"
-      proof-prf
+     ["Find theorems"
+      proof-find-theorems
       :active (proof-shell-live-buffer)]
      ["Start proof assistant"
       proof-shell-start
@@ -1751,7 +1766,9 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
 (define-key map [(control c) (control z)] 'proof-frob-locked-end)
 (define-key map [(control c) (control p)] 'proof-prf)
 (define-key map [(control c) ?c]	  'proof-ctxt)
-(define-key map [(control c) ?h]	  'proof-help)
+;; NB: next binding overwrites comint-find-source-code.  Anyone miss it?
+(define-key map [(control c) (control f)] 'proof-find-theorems)
+(define-key map [(control c) ?f]	  'proof-help)
 ;; FIXME: not implemented yet 
 ;; (define-key map [(meta p)]		  'proof-previous-matching-command)
 ;; (define-key map [(meta n)]		  'proof-next-matching-command)
@@ -1915,7 +1932,7 @@ finish setup which depends on specific proof assistant configuration."
 ;; proof-script.el ends here.
 
 ;; 
-;;; Local Variables:
+;;; Lo%al Va%iables:
 ;;; eval: (put 'proof-if-setting-configured 'lisp-indent-function 1)
 ;;; eval: (put 'proof-define-assistant-command 'lisp-indent-function 'defun)
 ;;; eval: (put 'proof-define-assistant-command-wtharg 'lisp-indent-function 'defun)