Indentation is a bit more accurate.

2 files changed, 85 insertions, 61 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 05fd9cb6..de331372 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -382,9 +382,9 @@ Lemma foo: forall n,
         ;; Having "return" here rather than as a separate rule in `exp' causes
         ;; it to be indented at a different level than "with".
         (matchexp (exp) (exp "as match" exp) (exp "in match" exp) (exp "return" exp) )
-        (assigns (exp ":=" exp) (assigns ";" assigns))
+        (assigns (exp ":= let" exp) (assigns ";" assigns))
         (exps (exp) (exps "," exps))
-        (expss (exps) (expss ";" expss) (expss "as" expss))
+        (expss (exps) (exps ":= record" exps) (expss ";" expss) (expss "as" expss))
         (expsss (expss) (expsss "=>" expsss))
         (expssss (expsss) (expssss "|" expssss))
         ;; The elements below are trying to capture the syntactic structure
@@ -398,16 +398,16 @@ Lemma foo: forall n,
                  ("Proof" subcmds "Proof End")
                  ("Module" subcmds "End")
                  ("Section" subcmds "End"))
-        (cmds ("Add" exp ":=" exp)
-              ("Lemma" exp ":=" exp)
-              ("Theorem" exp ":=" exp)
-              ("Instance" exp ":=" exp)
-              ("Class" exp ":=" exp)
-              ("Definition" exp ":=" exp)
-              ("Let" exp ":=" exp)
+        (cmds ("Add" exp ":=" exp) ("Add" exp) 
+              ("Lemma" exp ":=" exp) ("Lemma" exp)
+              ("Theorem" exp ":=" exp) ("Theorem" exp)
+              ("Instance" exp ":=" exp) ("Instance" exp)
+              ("Class" exp ":=" exp) ("Class" exp)
+              ("Definition" exp ":=" exp) ("Definition" exp)
+              ("Let" exp ":=" exp) ("Let" exp)
               ("Function" exp ":=" exp)
-              ("Fixpoint" exp ":=" exp)
-              ("Inductive" exp ":= inductive")
+              ("Program Fixpoint" exp ":=" exp) ("Fixpoint" exp ":=" exp)
+              ("Inductive" exp ":= inductive" expssss)
               ("CoInductive" exp ":= inductive" expssss)
               ("Notation" exp ":=" exp)
               ("Record" exp ":=" exp)
@@ -431,14 +431,15 @@ Lemma foo: forall n,
         (assoc ">") (assoc ">=") (assoc "<") (assoc "<=")
         (left "<>") (left "=") (left "==")
         (nonassoc "else")
-        (nonassoc "in") (assoc "in tactic") (left "=>"))
+        (nonassoc "in") (assoc "in tactic")  (left ":= record") (left "=>"))
       ;;'((nonassoc "return") (nonassoc "in match") (nonassoc "as match"))
       '((assoc ",")(assoc ";")(right "as")(assoc "|")(left "=>"))
       '((left "- bullet") (left "+ bullet") (left "* bullet"))
       '((assoc ".")))))
   "Parsing table for Coq.  See `smie-grammar'.")
 
-(defun coq-smie-search-token-forward (tokens &optional end)
+
+(defun coq-smie-search-token-forward (tokens &optional end ignore-between)
   "Search for one of TOKENS between point and END.
 Token \".\" is considered only if followed by a space."
   (unless end (setq end (point-max)))
@@ -446,16 +447,20 @@ Token \".\" is considered only if followed by a space."
       (catch 'found
         (while (< (point) end)
           ;; The default lexer is faster and is good enough for our needs.
-          (let ((next (smie-default-forward-token)))
-            ;; Do not consider "." when not followed by a space
-            (when (or (not (equal next "."))
-                      (looking-at "[[:space:]]"))
-              (cond
-               ((zerop (length next)) (forward-sexp 1))
-               ((member next tokens) (throw 'found next)))))))
+          (let* ((next (smie-default-forward-token))
+                 (parop (assoc next ignore-between)))
+            (if parop ; if we find something to ignore, we directly
+                                        ; go to corresponding closer
+                (coq-smie-search-token-forward (cons (cdr parop) nil) end ignore-between)
+              ;; Do not consider "." when not followed by a space
+              (when (or (not (equal next "."))
+                        (looking-at "[[:space:]]"))
+                (cond
+                 ((zerop (length next)) (forward-sexp 1))
+                 ((member next tokens) (throw 'found next))))))))
     (scan-error nil)))
 
-(defun coq-smie-search-token-backward (tokens &optional end)
+(defun coq-smie-search-token-backward (tokens &optional end ignore-between)
   "Search for one of TOKENS between point and END.
 Token \".\" is considered only if followed by a space."
   (unless end (setq end (point-min)))
@@ -463,13 +468,17 @@ Token \".\" is considered only if followed by a space."
       (catch 'found
         (while (> (point) end)
           ;; The default lexer is faster and is good enough for our needs.
-          (let ((next (smie-default-backward-token)))
-            ;; Do not consider "." when not followed by a space
-            (when (or (not (equal next "."))
-                      (looking-at ".[[:space:]]"))
-              (cond
-               ((zerop (length next)) (forward-sexp -1))
-               ((member next tokens) (throw 'found next)))))))
+          (let* ((next (smie-default-backward-token))
+                 (parop (rassoc next ignore-between)))
+            (if parop ; if we find something to ignore, we directly
+                                        ; go to corresponding closer
+                (coq-smie-search-token-backward (cons (car parop) nil) end ignore-between)
+              ;; Do not consider "." when not followed by a space
+              (when (or (not (equal next "."))
+                        (looking-at ".[[:space:]]"))
+                (cond
+                 ((zerop (length next)) (forward-sexp -1))
+                 ((member next tokens) (throw 'found next))))))))
     (scan-error nil)))
 
 
@@ -613,12 +622,16 @@ Token \".\" is considered only if followed by a space."
       (if (looking-at "{") "BeginSubproof" "EndSubproof"))
      ((and (equal tok "") (looking-back "|}" (- (point) 2)))
       (goto-char (match-beginning 0)) "|}")
-     ((and (equal tok ":=")
-           (save-excursion
-             (member (coq-smie-search-token-backward
-                      '("let" "Inductive" "Coinductive" "."))
-                     '("Inductive" "CoInductive"))))
-      ":= inductive")
+
+     ((equal tok ":=")
+      (save-excursion
+        (let ((corresp (coq-smie-search-token-backward
+                        '("let" "Inductive" "Coinductive" "{|" ".") nil '(("let" . ":=")))))
+          (cond
+           ((member corresp '("Inductive" "CoInductive")) ":= inductive")
+           ((equal corresp "let") ":= let")
+           ((or (looking-back "{")) ":= record")
+           (t tok)))))
      ((equal tok "*.") (forward-char 1) ".") ; for "auto with *."
      ((and (member tok '("+" "-" "*"))
            (save-excursion
@@ -699,9 +712,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
       ((equal token "return") 2)
       ((equal token "as") 2)
       ((and (equal token ";")
-            (smie-rule-parent-p "." "[" "]" "BeginSubproof" "EndSubproof" "|"))
-       2)
-     ;((member token '(":=")) 0)
+            (smie-rule-parent-p "." "{|" "[" "]" "BeginSubproof" "EndSubproof" "|"))
+       (smie-rule-separator kind))
+     ((member token '(":= inductive")) 2)
       ((and (equal token ",")
             (not (smie-rule-parent-p "forall" "quantif exists"))) 0)))
     (:before
@@ -712,9 +725,13 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
       ((equal token "as") 2)
       ((member token '("return" "in match" "as match")) (if (smie-rule-parent-p "match") 3))
       ((equal token "|")
-       (if (smie-rule-prev-p "with match")
-           (- (funcall smie-rules-function :after "with match") 2)
-         (smie-rule-separator kind)))
+       (cond ((smie-rule-prev-p "with match")
+              (- (funcall smie-rules-function :after "with match") 2))
+             ((smie-rule-prev-p ":= inductive")
+              (- (funcall smie-rules-function :after ":= inductive") 2))
+             (t (smie-rule-separator kind)))
+         ;(smie-rule-separator kind)
+         )
 ;      ((and (equal token ":=")
 ;            (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive"
 ;                                "Function" "Let" "Record" "Instance" "Class"
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 80b7313b..72f1d4f6 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -9,6 +9,13 @@ Record a : Type := make_a {
                        aa : nat
                      }.
 
+Inductive test : nat -> Prop :=
+| C1 : forall n, test n
+| C2 : forall n, test n
+| C3 : forall n, test n
+| C4 : forall n, test n.
+
+
 Lemma toto:nat.
 Proof.
   {{
@@ -96,8 +103,8 @@ Module M1'.
           destruct n.
           {
             idtac;[
-                     auto
-                   ].
+              auto
+            ].
           }
           auto.
         } 
@@ -150,16 +157,16 @@ End M1''.
 
 
 Record rec:Set := { 
-                 fld1:nat;
-                 fld2:nat;
-                 fld3:bool
-               }.
+    fld1:nat;
+    fld2:nat;
+    fld3:bool
+  }.
 
 Class cla {X:Set}:Set := { 
-                        cfld1:nat;
-                        cld2:nat;
-                        cld3:bool
-                      }.
+    cfld1:nat;
+    cld2:nat;
+    cld3:bool
+  }.
 
 
 
@@ -194,12 +201,12 @@ Module X.
     intros r.  
     {{
        idtac;
-         exists 
-           {|
-             fld1:=r.(fld2);
-             fld2:=r.(fld1);
-             fld3:=false
-           |}.
+       exists 
+         {|
+           fld1:=r.(fld2);
+           fld2:=r.(fld1);
+           fld3:=false
+         |}.
        (* ltac *)
        match goal with
          | _:rec |- ?a /\ ?b => split
@@ -226,17 +233,17 @@ Module foo.
   Proof.
     firstorder.
   Qed.
-
-
+  
+  
   Program Fixpoint f (x:nat) {struct x} : nat :=
     match x with
       | 0 => 0
       | S y => S (f y)
     end.
-
+  
   Program Instance all_iff_morphism {A : Type} :
     Proper (pointwise_relation A iff ==> iff) (@all A).
-
+  
   Next Obligation.
     Proof.
       unfold pointwise_relation, all in * .
@@ -255,7 +262,7 @@ Section SET.
   
   Require Import Program.
   
-
+  
   Definition eq_n : forall A n (v:Vector.t A n) n', n=n' -> Vector.t A n'.
   Proof.
     intros A n v n' H.