added match...with automatic building from atype name.

Had to correct a bug in proof-shell.

4 files changed, 34 insertions, 23 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3ac517f1..3c09968b 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -162,11 +162,11 @@
      ["Inductive3            indv3<C-BS>" (holes-insert-and-expand "indv3") t]
      ["Inductive4            indv4<C-BS>" (holes-insert-and-expand "indv4") t]
      ""
-     ["Section..." coq-insert-section t]
+     ["Section/Module (interactive)..." coq-insert-section-or-module t]
      ""
      ("Modules"
       "COMMAND               ABBREVIATION"
-      ["Module (interactive)... " coq-insert-module t]
+      ["Module (interactive)... " coq-insert-section-or-module t]
       ["Module                mo<C-BS>" (holes-insert-and-expand "mo") t]
       ["Module (<:)           mo2<C-BS>" (holes-insert-and-expand "mo") t]
 ;      ["Module (interactive)  moi<C-BS>" (holes-insert-and-expand "moi") t]
@@ -224,6 +224,7 @@
      ["if then else  if<C-BS>"  (holes-insert-and-expand "if") t]
      ["let in        li<C-BS>"  (holes-insert-and-expand "li") t]
      ""
+     ["match (smart)        "  coq-match t]
      ["match         m<C-BS>"  (holes-insert-and-expand "m") t]
      ["match2        m2<C-BS>"  (holes-insert-and-expand "m2") t]
      ["match3        m3<C-BS>"  (holes-insert-and-expand "m3") t]
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index adac6527..f69c3429 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -137,7 +137,6 @@
 )
 
 (defun find-reg (lim reg)
-  (message "findreg")
   (let ((limit lim))
 	 (if (< limit (point)) ;swap limit and point
 		  (let ((x limit)) (setq limit (point)) (goto-char x)))
diff --git a/coq/coq.el b/coq/coq.el
index 1976ac28..c43ab80e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -116,29 +116,25 @@ To disable coqc being called (and use only make), set this to nil."
 
 (require 'coq-abbrev)
 
-(defun coq-insert-section (s)
-  (interactive  "sSection name: ")
-  (let ((p (point)))
-    (insert "Section " s ".\n#\nEnd " s ".")
-    (holes-replace-string-by-holes-backward p)
-    (goto-char p)
-    (holes-set-point-next-hole-destroy))
-)
-
 (defconst module-kinds-table 
-  '(("Module" 1) ("Module Type" 2) ("Declare Module" 3))
+  '(("Section" 0) ("Module" 1) ("Module Type" 2) ("Declare Module" 3))
   "Enumerates the different kinds of modules.")
 
 (defconst modtype-kinds-table
   '(("" 1) (":" 2) ("<:" 3))
   "Enumerates the different kinds of type information for modules.")
 
-(defun coq-insert-module ()
+(defun coq-insert-section-or-module ()
+  "Insert a module or a section after asking right questions."
   (interactive)
-  (let* ((mods (completing-read "kind of module (tab to see list): " module-kinds-table))
-         (s (read-string  "Module name: "))
-         (typkind (completing-read "kind of type (optional, tab to see list): " modtype-kinds-table))
-         (p (point)))
+  (let* 
+      ((mods (completing-read "kind of module (tab to see list): " module-kinds-table))
+       (s (read-string  "Name: "))
+       (typkind (if (string-equal mods "Section")
+                    "" ;; if not a section
+                  (completing-read "kind of type (optional, tab to see list): " 
+                                   modtype-kinds-table)))
+       (p (point)))
     (if (string-equal typkind "")
         (progn
           (insert mods " " s ".\n#\nEnd " s ".")
@@ -623,7 +619,7 @@ This is specific to `coq-mode'."
   "Ask for an ident and print the corresponding term."
   (let (cmd)
     (proof-shell-ready-prover) 
-    (setq cmd (coq-guess-or-ask-for-string "ask"))
+    (setq cmd (coq-guess-or-ask-for-string ask))
     (proof-shell-invisible-command
      (format (concat do " %s. ") cmd)))  
   ) 
@@ -706,12 +702,29 @@ Based on idea mentioned in Coq reference manual."
         (insert intros)
         (indent-region start (point) nil)))))
 
+(defun coq-match ()
+  "Insert a match expression from a type name by Show Intros.
+Based on idea mentioned in Coq reference manual."
+  (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 "."))))
+      ;; 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))))))
+
+
 (proof-defshortcut coq-Apply         "Apply "   [(control ?a)])
 
 ;(proof-defshortcut coq-begin-Section "Section " [(control ?s)])
 (define-key coq-keymap [(control ?i)] 'coq-intros)
-(define-key coq-keymap [(control ?s)] 'coq-insert-section)
-(define-key coq-keymap [(control ?m)] 'coq-insert-module)
+(define-key coq-keymap [(control ?s)] 'coq-insert-section-or-module)
+(define-key coq-keymap [(control ?m)] 'coq-match)
 (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)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index acb70b7e..62f61ddd 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1953,10 +1953,8 @@ string instead.
 Errors are not supressed and will result in a display as 
 usual, unless NOERROR is non-nil."
   (setq proof-shell-no-response-display t)
-  (setq proof-shell-no-error-display t)
   (unwind-protect
       (proof-shell-invisible-command cmd 'waitforit)
-    (setq proof-shell-no-error-display nil)
     (setq proof-shell-no-response-display nil))
   proof-shell-last-output)