diff options
| -rw-r--r-- | coq/coq-abbrev.el | 16 | ||||
| -rw-r--r-- | coq/coq.el | 52 |
2 files changed, 38 insertions, 30 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index c73b4e4d..3ac517f1 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -5,7 +5,7 @@ (interactive) (describe-variable 'holes-doc)) -;#s are replaced by holes by holes-abbrev-complete +;#s and @{..} are replaced by holes by holes-abbrev-complete (if (boundp 'holes-abbrev-complete) () (define-abbrev-table 'coq-mode-abbrev-table @@ -267,6 +267,7 @@ ["generalize g<C-BS>" (holes-insert-and-expand "g") t] ["induction ind<C-BS>" (holes-insert-and-expand "ind") t] ["injection inj<C-BS>" (holes-insert-and-expand "inj") t] + ["intro (smart)" coq-intros t] ["intro i<C-BS>" (holes-insert-and-expand "i") t] ["intros is<C-BS>" (holes-insert-and-expand "is") t] ["intuition intu<C-BS>" (holes-insert-and-expand "intu") t] @@ -297,10 +298,11 @@ ;; FIXME: submenus should be split off here. Also, these commands ;; should only be available when a proof is open. ("Show" - ["Show ith goal..." coq-Show t] - ["Show Tree" coq-show-tree t] - ["Show Proof" coq-show-proof t] - ["Show Conjectures" coq-show-conjectures t]) ;; maybe not so useful with editing in PG? + ["ith goal..." coq-Show t] + ["Tree" coq-show-tree t] + ["Proof" coq-show-proof t] + ["Conjectures" coq-show-conjectures t] ;; maybe not so useful with editing in PG? + ["Hints" coq-PrintHint t]) ("Holes" ;; da: I tidied this menu a bit. I personally think this "trick" @@ -333,8 +335,10 @@ :selected (and (boundp 'abbrev-mode) abbrev-mode)]) ;; With all these submenus you have to wonder if these things belong ;; on the main menu. Are they the most often used? - ["Insert intros" coq-intros t] + ["Smart intros" coq-intros t] ["Print..." coq-Print t] + ["Print Implicit..." coq-Print t] + ["About..." coq-About t] ["Check..." coq-Check t] ["Hints" coq-PrintHint t] ["Search isos/pattern..." coq-SearchIsos t] @@ -605,46 +605,51 @@ This is specific to `coq-mode'." (interactive) (let (cmd) (proof-shell-ready-prover) - (setq cmd (read-string "SearchPattern: " nil 'proof-minibuffer-history)) + (setq cmd (read-string "SearchPattern ex: (?X1 + _ = _ + ?X1) : " "(" 'proof-minibuffer-history)) (proof-shell-invisible-command (format "SearchPattern %s. " cmd)))) (defun coq-guess-or-ask-for-string (s) (let ((guess - (if (region-exists-p) - (buffer-substring-no-properties (region-beginning) (region-end)) - (symbol-near-point)))) - (read-string - (if guess (concat s " (" guess "):")(concat s ":")) - nil 'proof-minibuffer-history guess)) + (if (region-exists-p) + (buffer-substring-no-properties (region-beginning) (region-end)) + (symbol-near-point)))) + (read-string + (if guess (concat s " (" guess "):")(concat s ":")) + nil 'proof-minibuffer-history guess)) ) -(defun coq-Print () +(defun coq-ask-do (ask do) "Ask for an ident and print the corresponding term." - (interactive) (let (cmd) (proof-shell-ready-prover) - (setq cmd (coq-guess-or-ask-for-string "Print")) + (setq cmd (coq-guess-or-ask-for-string "ask")) (proof-shell-invisible-command - (format "Print %s. " cmd)))) + (format (concat do " %s. ") cmd))) + ) + +(defun coq-Print () "Ask for an ident and print the corresponding term." + (interactive) + (coq-ask-do "Print: " "Print")) + +(defun coq-About () "Ask for an ident and print information on it." + (interactive) + (coq-ask-do "About: " "About")) + +(defun coq-Print-implicit () + "Ask for an ident and print the corresponding term." + (interactive) + (coq-ask-do "Print Implicit: " "Print Implicit")) (defun coq-Check () "Ask for a term and print its type." (interactive) - (let (cmd) - (proof-shell-ready-prover) - (setq cmd (coq-guess-or-ask-for-string "Check")) - (proof-shell-invisible-command - (format "Check %s. " cmd)))) + (coq-ask-do "Check: " "Check")) (defun coq-Show () "Ask for a number i and show the ith goal." (interactive) - (let (cmd) - (proof-shell-ready-prover) - (setq cmd (read-string "Show Goal number: " nil 'proof-minibuffer-history)) - (proof-shell-invisible-command - (format "Show %s. " cmd)))) + (coq-ask-do "Show goal number: " "Show")) (proof-definvisible coq-PrintHint "Print Hint. ") @@ -653,9 +658,7 @@ This is specific to `coq-mode'." (proof-definvisible coq-show-tree "Show Tree.") (proof-definvisible coq-show-proof "Show Proof.") (proof-definvisible coq-show-conjectures "Show Conjectures.") -(proof-definvisible coq-show-intros "Show Intros.") -;; Coq ref manual says of show intro: "with an appropriate Proof General macro"... can -;; we have it to add to PG, please? +(proof-definvisible coq-show-intros "Show Intros.") ; see coq-intros below (defun coq-PrintHint () @@ -712,6 +715,7 @@ Based on idea mentioned in Coq reference manual." (define-key coq-keymap [(control ?e)] 'coq-end-Section) (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) +(define-key coq-keymap [(control ?b)] 'coq-About) (define-key coq-keymap [(control ?c)] 'coq-Check) (define-key coq-keymap [(control ?h)] 'coq-PrintHint) ;; da: I've moved this three buffer layout into the main code now, |