Fix #562. Lazy/multi_?match indentation support.

Actually it seems that even multimatch and lazymatch was poorly
supported.

2 files changed, 25 insertions, 20 deletions

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 37dc390c..39c68428 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -172,7 +172,7 @@ attention to case differences."
   (let ((case-fold-search nil))
     (save-excursion
       (coq-find-real-start)
-      (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac\\|Tactic\\s-+Notation\\)\\s-"))))
+      (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac2?\\|Tactic\\s-+Notation\\)\\s-"))))
 
 (defun coq-smie-is-inside-parenthesized-tactic ()
   (and (coq-smie-is-tactic) ;; fragile (uppercase test only)
@@ -239,7 +239,7 @@ the token of \".\" is simply \".\"."
 
 
 (defun coq-smie-find-unclosed-match-backward ()
-  (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" "."))))
+  (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" "lazy_match" "mult_match" "."))))
     (cond
      ((null tok) nil)
      ((equal tok ".") nil)
@@ -493,8 +493,7 @@ The point should be at the beginning of the command name."
       ;; we can.
       (save-excursion (coq-smie-backward-token)))
 
-     ;; easier to return directly than calling coq-smie-backward-token
-     ((member tok '("lazymatch" "multimatch")) "match")
+     ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match")
 
      ;; detect "with signature", otherwies use coq-smie-backward-token
      ((equal tok "with")
@@ -629,7 +628,7 @@ The point should be at the beginning of the command name."
      ((equal tok ",")
       (save-excursion
 	(let ((backtok (coq-smie-search-token-backward
-			'("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" "."))))
+			'("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" "lazy_match" "multi_match" "."))))
 	  (cond
 	   ((member backtok '("forall" "∀" "∃")) ", quantif")
 	   ((equal backtok "exists") ; there is a tactic called exists
@@ -645,9 +644,9 @@ The point should be at the beginning of the command name."
      ;; trying to discriminate between bollean operator || and tactical ||.
      ((equal tok "||")
       (save-excursion
-	(let ((backtok (coq-smie-search-token-backward '("." ";" "Ltac" "(" "[" "{"))))
+	(let ((backtok (coq-smie-search-token-backward '("." ";" "Ltac" "Ltac2" "(" "[" "{"))))
 	  (cond
-	   ((member backtok '("." "Ltac")) "|| tactic")
+	   ((member backtok '("." "Ltac" "Ltac2")) "|| tactic")
 	   ((and (equal backtok ";")
 		 (or (forward-char) t)
 		 (equal (coq-smie-backward-token) "; tactic")) ;; recursive
@@ -697,7 +696,7 @@ The point should be at the beginning of the command name."
 	;(coq-find-real-start)
 	(coq-smie-module-deambiguate)))
 
-     ((member tok '("lazymatch" "multimatch")) "match")
+     ((member tok '("lazy_?match" "multi_?match")) "match")
 
      ((equal tok "tryif") "if")
 
@@ -734,7 +733,7 @@ The point should be at the beginning of the command name."
      ;;  (forward-char -1)
      ;;  (if (looking-at "{") "{ subproof" "} subproof"))
 
-     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)"
+     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac2?\\|uconstr\\)"
                                          (- (point) 7)))
       ": ltacconstr")
 
@@ -745,8 +744,8 @@ The point should be at the beginning of the command name."
      ((equal tok "=>")
       (save-excursion
 	(let ((corresp (coq-smie-search-token-backward
-			'("|" "match" "lazymatch" "multimatch" "fun" ".")
-			nil '((("match" "lazymatch" "multimatch") . "end") ("fun" . "=>")))))
+			'("|" "match" "lazymatch" "multimatch" "lazy_match" "multi_match" "fun" ".")
+			nil '((("match" "lazy_match" "multi_match") . "end") ("fun" . "=>")))))
 	  (cond
 	   ((member corresp '("fun")) "=> fun") ; fun
 	   (t tok)))))
@@ -803,12 +802,12 @@ The point should be at the beginning of the command name."
       (save-excursion
 	(let ((prev-interesting
 	       (coq-smie-search-token-backward
-		'("match" "lazymatch" "multimatch" "Morphism" "Relation" "." ". proofstart"
+		'("match" "lazymatch" "multimatch" "lazy_match" "multi_match" "Morphism" "Relation" "." ". proofstart"
 		  "{ subproof" "} subproof" "as")
 		nil
-		'((("match" "lazymatch" "multimatch" "let") . "with") ("with" . "signature")))))
+		'((("match" "lazy_match" "multi_match" "let") . "with") ("with" . "signature")))))
 	  (cond
-	   ((member prev-interesting '("match" "lazymatch" "multimatch")) "as match")
+	   ((member prev-interesting '("match" "lazymatch" "multimatch" "lazy_match" "mult_match")) "as match")
 	   ((member prev-interesting '("Morphism" "Relation")) "as morphism")
 	   (t tok)))))
 
@@ -834,9 +833,9 @@ The point should be at the beginning of the command name."
       (save-excursion
 	(let ((prev-interesting
 	       (coq-smie-search-token-backward
-		'("let" "match" "lazymatch" "multimatch" ;"eval" should be "eval in" but this is not supported by search-token-backward
+		'("let" "match" "lazymatch" "multimatch" "lazy_match" "mult_match" ;"eval" should be "eval in" but this is not supported by search-token-backward
 		  "." ) nil
-		'((("match" "lazymatch" "multimatch") . "with") (("let" ;"eval"
+		'((("match" "lazymatch" "multimatch" "lazy_match" "mult_match") . "with") (("let" ;"eval"
 				       ) . "in")))))
 	  (cond
 	   ((member prev-interesting '("." nil)) "in tactic")
@@ -875,6 +874,10 @@ The point should be at the beginning of the command name."
       (let ((newtok (coq-smie-backward-token))) ; recursive call
 	(concat newtok "." tok)))
 
+     ;; easier to return directly than calling coq-smie-backward-token
+     ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match")
+
+
      ((coq-dot-friend-p tok) ".")
      (tok))))
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 0e143637..a517df71 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -236,14 +236,16 @@ so for the following reasons:
      ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear")
      ("lapply" "lap" "lapply" t "lapply")
      ("lazy" "lazy" "lazy beta delta [#] iota zeta" t "lazy")
-     ("lazymatch with" "m" "lazymatch # with\n| # => #\nend")
+     ("lazymatch with" "lazym" "lazymatch # with\n| # => #\nend")
+     ("lazy_match! with" "lazy_m" "lazy_match! # with\n| # => #\nend")
      ("left" "left" "left" t "left")
      ("lia" nil "lia" t "lia")
      ("linear" "lin" "linear" t "linear")
      ("load" "load" "load" t "load")
      ("lra" nil "lra" t "lra")
      ("move after" "mov" "move # after #" t "move")
-     ("multimatch with" "m" "multimatch # with\n| # => #\nend")
+     ("multimatch with" "mm" "multimatch # with\n| # => #\nend")
+     ("multi_match! with" "multi_m" "multi_match! # with\n| # => #\nend")
      ("nia" nil "nia" t "nia")
      ("now_show" nil "now_show" t "now_show")
      ("nra" nil "nra" t "nra")
@@ -955,7 +957,7 @@ so for the following reasons:
     ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #")
     ("if" "if" "if # then # else #" nil "if")
     ("let in" "li" "let # := # in #" nil "let")
-    ("match! (from type)" nil "" nil "match" coq-insert-match)
+    ("match?" nil "" nil "match" coq-insert-match)
     ("match with" "m" "match # with\n| # => #\nend")
     ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend")
     ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend")
@@ -1172,7 +1174,7 @@ It is used:
   (append
    '(
      "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match"
-     "lazymatch" "multimatch"
+     "lazymatch" "multimatch" "lazy_match" "multi_match"
      "return" "struct" "else" "end" "if" "in" "into" "let" "then"
      "using" "with" "beta" "delta" "iota" "zeta" "after" "until"
      "at" "Sort" "Time" "dest" "where"