Fixed lazymatch and multimatch indentation/highlighting.

3 files changed, 60 insertions, 38 deletions

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 06cc2582..2d48a592 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -136,14 +136,15 @@ the token of \".\" is simply \".\"."
 
 
 (defun coq-smie-find-unclosed-match-backward ()
-  (let ((tok (coq-smie-search-token-backward '("with" "match" "."))))
+  (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" "."))))
     (cond
      ((null tok) nil)
      ((equal tok ".") nil)
-     ((equal tok "match") t)
      ((equal tok "with")
       (coq-smie-find-unclosed-match-backward)
-      (coq-smie-find-unclosed-match-backward)))))
+      (coq-smie-find-unclosed-match-backward))
+     (t t) ;; all variants of match
+     )))
 
 ;; point supposed to be at start of the "with"
 (defun coq-smie-with-deambiguate()
@@ -436,7 +437,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" "."))))
+			'("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" "."))))
 	  (cond
 	   ((member backtok '("forall" "∀" "∃")) ", quantif")
 	   ((equal backtok "exists") ; there is a tactic called exists
@@ -474,6 +475,8 @@ The point should be at the beginning of the command name."
 	;(coq-find-real-start)
 	(coq-smie-module-deambiguate)))
 
+     ((member tok '("lazymatch" "multimatch")) "match")
+
      ;; rhaaa... Some peolple use "End" as a id...
      ((equal tok "End")
       (if (coq-is-at-command-real-start) "end module" tok))
@@ -499,8 +502,8 @@ The point should be at the beginning of the command name."
      ((equal tok "=>")
       (save-excursion
 	(let ((corresp (coq-smie-search-token-backward
-			'("|" "match" "fun" ".")
-			nil '(("match" . "end") ("fun" . "=>")))))
+			'("|" "match" "lazymatch" "multimatch" "fun" ".")
+			nil '((("match" "lazymatch" "multimatch") . "end") ("fun" . "=>")))))
 	  (cond
 	   ((member corresp '("fun")) "=> fun") ; fun
 	   (t tok)))))
@@ -550,12 +553,12 @@ The point should be at the beginning of the command name."
       (save-excursion
 	(let ((prev-interesting
 	       (coq-smie-search-token-backward
-		'("match" "Morphism" "Relation" "." ". proofstart"
+		'("match" "lazymatch" "multimatch" "Morphism" "Relation" "." ". proofstart"
 		  "{ subproof" "} subproof" "as")
 		nil
-		'((("match" "let") . "with") ("with" . "signature")))))
+		'((("match" "lazymatch" "multimatch" "let") . "with") ("with" . "signature")))))
 	  (cond
-	   ((equal prev-interesting "match") "as match")
+	   ((member prev-interesting '("match" "lazymatch" "multimatch")) "as match")
 	   ((member prev-interesting '("Morphism" "Relation")) "as morphism")
 	   (t tok)))))
 
@@ -581,9 +584,9 @@ The point should be at the beginning of the command name."
       (save-excursion
 	(let ((prev-interesting
 	       (coq-smie-search-token-backward
-		'("let" "match" ;"eval" should be "eval in" but this is not supported by search-token-backward
+		'("let" "match" "lazymatch" "multimatch" ;"eval" should be "eval in" but this is not supported by search-token-backward
 		  "." ) nil
-		'(("match" . "with") (("let" ;"eval"
+		'((("match" "lazymatch" "multimatch") . "with") (("let" ;"eval"
 				       ) . "in")))))
 	  (cond
 	   ((member prev-interesting '("." nil)) "in tactic")
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b817aafe..8c728284 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -225,10 +225,12 @@ 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")
      ("left" "left" "left" t "left")
      ("linear" "lin" "linear" t "linear")
      ("load" "load" "load" t "load")
      ("move after" "mov" "move # after #" t "move")
+     ("multimatch with" "m" "multimatch # with\n| # => #\nend")
      ("now_show" nil "now_show" t "now_show")     
      ("omega" "o" "omega" t "omega")
      ("pattern" "pat" "pattern" t "pattern")
@@ -875,6 +877,7 @@ It is used:
    coq-user-reserved-db
    '(
      "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match"
+     "lazymatch" "multimatch"
      "return" "struct" "else" "end" "if" "in" "into" "let" "then"
      "using" "with" "beta" "delta" "iota" "zeta" "after" "until"
      "at" "Sort" "Time" "dest" "where"
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index edf1a536..27b64942 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -88,9 +88,9 @@ End Y.
 
 Function div2 (n : nat) {struct n}: nat :=
   match n with
-    | 0 => 0
-    | 1 => 0
-    | S (S n') => S (div2 n')
+  | 0 => 0
+  | 1 => 0
+  | S (S n') => S (div2 n')
   end.
 
 
@@ -257,9 +257,25 @@ Module X.
           |}.
         (* ltac *)
         match goal with
-          | _:rec |- ?a /\ ?b => split
-          | _ => fail
+        | _:rec |- ?a /\ ?b => split
+        | _ => fail
+        end.
+
+        match goal with
+          _:rec |- ?a /\ ?b => split
+        | _ => fail
+        end.
+
+        lazymatch goal with
+          _:rec |- ?a /\ ?b => split
+        | _ => fail
+        end.
+
+        multimatch goal with
+          _:rec |- ?a /\ ?b => split
+        | _ => fail
         end.
+
         { simpl. auto. }
         { simpl. auto. }}}
   Qed.
@@ -285,8 +301,8 @@ Module TC.
   
   Program Fixpoint f (x:nat) {struct x} : nat :=
     match x with
-      | 0 => 0
-      | S y => S (f y)
+    | 0 => 0
+    | S y => S (f y)
     end.
   
   Program Instance all_iff_morphism {A : Type} :
@@ -321,26 +337,26 @@ Section SET.
   Fixpoint setVecProd (T : Type) (n : nat) (v1:Vector.t (set T) n) {struct v1}:
     (Vector.t T n) ->  Prop :=
     match v1 with
-        Vector.nil =>
-        fun v2 =>
-          match v2 with 
-              Vector.nil => True
-            | _ => False
-          end
-      | (Vector.cons x n' v1') =>
-        fun v2 =>
-          (* indentation of dependen "match" clause. *)
-          match v2
-                as
-                X
-                in
-                Vector.t _ n''
-                return
-                (Vector.t T (pred n'') -> Prop) -> Prop
-          with 
-            | Vector.nil => fun _ => False 
-            | (Vector.cons y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
-          end (setVecProd T n' v1')
+      Vector.nil =>
+      fun v2 =>
+        match v2 with 
+          Vector.nil => True
+        | _ => False
+        end
+    | (Vector.cons x n' v1') =>
+      fun v2 =>
+        (* indentation of dependen "match" clause. *)
+        match v2
+              as
+              X
+              in
+              Vector.t _ n''
+              return
+              (Vector.t T (pred n'') -> Prop) -> Prop
+        with 
+        | Vector.nil => fun _ => False 
+        | (Vector.cons y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
+        end (setVecProd T n' v1')
     end.
   
 End SET.