From b851888514322ecaefc6898b8a74cbaf412982ce Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 9 Nov 2005 15:24:40 +0000
Subject: Added holes to "math...with" generation from a type name.

---
 coq/coq.el | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index c43ab80e..7e148af2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -704,19 +704,33 @@ Based on idea mentioned in Coq reference manual."
 
 (defun coq-match ()
   "Insert a match expression from a type name by Show Intros.
-Based on idea mentioned in Coq reference manual."
+Based on idea mentioned in Coq reference manual. Also insert holes at insertion
+positions."
   (interactive)
   (proof-shell-ready-prover) 
   (let* ((cmd))
     (setq cmd (read-string "Build match for type:"))
-    (let ((match 
-           (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd "."))))
+    (let* ((thematch 
+           (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd ".")))
+          (match (replace-in-string thematch "=> \n" "=> #\n")))
       ;; if error, it will be displayed in response buffer (see def of 
       ;; proof-shell-invisible-cmd-get-result), otherwise:
       (unless (proof-string-match coq-error-regexp match)
         (let ((start (point)))
           (insert match)
-          (indent-region start (point) nil))))))
+          (indent-region start (point) nil)
+          (let ((n (holes-replace-string-by-holes-backward start)))
+            (case n
+	(0 nil)				; no hole, stay here.
+	(1
+	 (goto-char start)
+	 (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
+	(t
+	 (goto-char start)
+	 (message 
+          (substitute-command-keys
+           "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc.")))))
+          )))))
 
 
 (proof-defshortcut coq-Apply         "Apply "   [(control ?a)])
-- 
cgit v1.2.3