Still fixing indentation details for coq.

1 files changed, 37 insertions, 44 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 97b9943a..c10357b2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -362,27 +362,18 @@ Lemma foo: forall n,
              ("if" exp "then" exp "else" exp)
              ("quantif exists" exp "," exp)
              ("forall" exp "," exp)
-             ("(" exps ")")
-             ("{|" exps "|}")
-             ("{" exps "}")
-             ("[" expssss "]")
-             (exp "<->" exp)
-             (exp "/\\" exp)
-             (exp "\\/" exp)
-             (exp "==" exp)
-             (exp "^" exp)
-             (exp "+" exp)
-             (exp "-" exp)
-             (exp "*" exp)
-             ;(exp "/" exp)
-             (exp "=" exp) (exp "<>" exp) (exp "<=" exp) (exp "<" exp) (exp ">=" exp) (exp ">" exp)
-             (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
-             (exp "->" exp)
+             ("(" exps ")") ("{|" exps "|}") ("{" exps "}") ("[" expssss "]")
+             (exp "<->" exp) (exp "/\\" exp) (exp "\\/" exp)
+             (exp "==" exp) (exp "^" exp) (exp "+" exp)
+             (exp "-" exp) (exp "*" exp) ;(exp "/" exp)
+             (exp "=" exp) (exp "<>" exp) (exp "<=" exp) (exp "<" exp)
+             (exp ">=" exp) (exp ">" exp) (exp "=?" exp) (exp "<=?" exp)
+             (exp "<?" exp) (exp "->" exp)
              (exp ":" exp))
         ;; 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 ":= let" exp) (assigns ";" assigns))
+        (assigns  (exp ":= let" exp) (assigns "; record" assigns))
         (exps (exp) (exps "," exps))
         (expss (exps) (exps ":= record" exps) (expss ";" expss) (expss "as" expss))
         (expsss (expss) (expsss "=>" expsss))
@@ -398,7 +389,7 @@ Lemma foo: forall n,
                  ("Proof" subcmds "Proof End")
                  ("Module" subcmds "End")
                  ("Section" subcmds "End"))
-        (cmds ("Add" exp ":=" exp) ("Add" exp) 
+        (cmds ("Add" exp ":=" exp) ("Add" exp)
               ("Lemma" exp ":=" exp) ("Lemma" exp)
               ("Theorem" exp ":=" exp) ("Theorem" exp)
               ("Instance" exp ":=" exp) ("Instance" exp)
@@ -421,19 +412,13 @@ Lemma foo: forall n,
               (cmds "." cmds)))
       ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
       ;; each line orders tokens by increasing proprity
-      '( 
-        (assoc ",") (assoc ":") (assoc "->")
-        (left "<->")
-        (left "^") 
-        (assoc "-")(assoc "+") (assoc "\\/")
-        (assoc "*") (assoc "/\\")
-        (assoc "<?") (assoc "<=?") (assoc "=?")
-        (assoc ">") (assoc ">=") (assoc "<") (assoc "<=")
-        (left "<>") (left "=") (left "==")
-        (nonassoc "else")
-        (nonassoc "in") (assoc "in tactic")  (left ":= record") (left "=>"))
-      ;;'((nonassoc "return") (nonassoc "in match") (nonassoc "as match"))
-      '((assoc ",")(assoc ";")(right "as")(assoc "|")(left "=>"))
+      '((assoc ",") (assoc ":") (assoc "->") (left "<->") (left "^")
+        (assoc "-")(assoc "+") (assoc "\\/") (assoc "*") (assoc "/\\")
+        (assoc "<?") (assoc "<=?") (assoc "=?") (assoc ">") (assoc ">=")
+        (assoc "<") (assoc "<=") (left "<>") (left "=") (left "==")
+        (nonassoc "else") (nonassoc "in") (assoc "in tactic")
+        (assoc ":= record") (assoc "; record") (left "=>"))
+      '((assoc ",")(assoc ";")(right "as")(left "|")(left "=>"))
       '((left "- bullet") (left "+ bullet") (left "* bullet"))
       '((assoc ".")))))
   "Parsing table for Coq.  See `smie-grammar'.")
@@ -525,7 +510,7 @@ Token \".\" is considered only if followed by a space."
         (let ((newtok (coq-smie-forward-token)))
           (concat tok newtok)))
        (t tok)))
-     ((member tok '(":=" "+" "-" "*" "with" "exists" "in" "as" "∀" "∃" "→"))
+     ((member tok '(":=" "+" "-" "*" "with" "exists" "in" "as" "∀" "∃" "→" ";"))
       ;; The important lexer for indentation's performance is the backward
       ;; lexer, so for the forward lexer we delegate to the backward one when
       ;; we can.
@@ -593,7 +578,10 @@ Token \".\" is considered only if followed by a space."
               (concat newtok tok))
             ".-selector"  ;; probably a user defined syntax
             ))))
-
+     ((equal tok ";")
+      (save-excursion
+        (if (equal (coq-smie-search-token-forward '("." "{")) ".")
+            tok "; record")))
      ((member tok '("Fixpoint" "Declaration" "Lemma" "Instance"))
       (let ((pos (point))
             (prev (smie-default-backward-token)))
@@ -665,21 +653,20 @@ Token \".\" is considered only if followed by a space."
         "Proof"))
      ((equal tok "as")
       (save-excursion
-        (let ((prev-interesting 
+        (let ((prev-interesting
                (coq-smie-search-token-backward
                 ;; coq-smie-search... do not stop on the "." of qualified.names
                 '("match" "as" "." ))))
           (cond
            ((member prev-interesting '("." "as")) "as")
            ((equal prev-interesting "match") "as match")
-           ))))     ;; "in" is for let and match .. as .. in ... "in tactic" is for rewrite in.
+           ))))
+     ;; three uses of "in": let, match .. as .. in ... and tactics
      ((equal tok "in")
       (save-excursion
-        (let ((prev-interesting 
+        (let ((prev-interesting
                (coq-smie-search-token-backward
-                ;; coq-smie-search... do not stop on the "." of qualified.names
-                '("in" "let" "match" "." ));;"eval" "rewrite" "unfold" "apply" "simpl" "compute" "symmetry"
-               ))
+                '("in" "let" "match" "." ))))
           (cond
            ((equal prev-interesting ".") "in tactic")
            ((member prev-interesting '("in" "let")) "in")
@@ -707,14 +694,20 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
       ;; Override the default indent step added because of their presence
       ;; in smie-closer-alist.
       ((equal token "with match") 4)
+      ((equal token ":") 2)
       ((equal token "in match") 2)
       ((equal token "as match") 2)
       ((equal token "return") 2)
       ((equal token "as") 2)
-      ((and (equal token ";")
-            (smie-rule-parent-p "." "{|" "[" "]" "BeginSubproof" "EndSubproof" "|"))
-       (smie-rule-separator kind))
-     ((member token '(":= inductive")) 2)
+      ((equal token "; record")
+       (cond
+        ((smie-rule-parent-p "; record") (smie-rule-separator kind))
+        (t (smie-rule-parent 2))))
+      ((equal token ";")
+       (cond
+        ((smie-rule-parent-p ";") (smie-rule-separator kind))
+        (t (smie-rule-parent 2))))
+      ((equal token ":= inductive") 2)
       ((and (equal token ",")
             (not (smie-rule-parent-p "forall" "quantif exists"))) 0)))
     (:before
@@ -725,7 +718,7 @@ 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 "|")
-       (cond ((smie-rule-prev-p "with match")
+       (cond ((smie-rule-parent-p "with match")
               (- (funcall smie-rules-function :after "with match") 2))
              ((smie-rule-prev-p ":= inductive")
               (- (funcall smie-rules-function :after ":= inductive") 2))