Summary: coq-smie: Do not assume all "." are terminators. Handle "Programs".

(coq-smie-grammar): Add "Function" rule.
(coq-smie-forward-token, coq-smie-backward-token): New functions.
(coq-mode-config): Use them for the SMIE lexer.

1 files changed, 45 insertions, 2 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 1558a82a..ad5f3684 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -250,6 +250,7 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3."
       (exps (exp) (exps "," exps))
       (decls ("Lemma" exp ":=" exp)
              ("Definition" exp ":=" exp)
+             ("Function" exp ":=" exp)
              ("Fixpoint" exp ":=" exp)
              ("Inductive" exp ":=" branches)
              ("Notation" exp ":=" exp)
@@ -265,6 +266,45 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3."
     '((assoc "|")) '((assoc ",")) '((assoc ";")) '((assoc ".")))))
   "Parsing table for Coq.  See `smie-grammar'.")
 
+(defun coq-smie-forward-token ()
+  (let ((tok (smie-default-forward-token)))
+    (cond
+     ((equal tok ".")
+      ;; Distinguish field-selector "." from terminator ".".
+      (if (or (looking-at "(")                ;Record selector.
+              (and (looking-at "[[:alpha:]]") ;Maybe qualified id.
+                   (save-excursion
+                     (goto-char (1- (point)))
+                     (skip-syntax-backward "w_")
+                     (looking-at "[[:upper:]]"))))
+          ".-selector" "."))
+     ((equal tok "Program")
+      (let ((pos (point))
+            (next (smie-default-forward-token)))
+        (if (member next '("Fixpoint" "Declaration" "Lemma"))
+            next
+          (goto-char pos)
+          tok)))
+     (tok))))
+
+(defun coq-smie-backward-token ()
+  (let ((tok (smie-default-backward-token)))
+    (cond
+     ((equal tok ".")
+      ;; Distinguish field-selector "." from terminator ".".
+      (if (or (looking-at "\\.(")             ;Record selector.
+              (and (looking-at "\\.[[:alpha:]]") ;Maybe qualified id.
+                   (save-excursion
+                     (skip-syntax-backward "w_")
+                     (looking-at "[[:upper:]]"))))
+          ".-selector" "."))
+     ((member tok '("Fixpoint" "Declaration" "Lemma"))
+      (let ((pos (point))
+            (prev (smie-default-backward-token)))
+        (unless (equal prev "Program") (goto-char pos))
+        tok))
+     (tok))))
+
 (defun coq-smie-rules (kind token)
   "Indentation rules for Coq.  See `smie-rules-function'."
   (case kind
@@ -281,7 +321,8 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3."
       ((equal token "return") (if (smie-rule-parent-p "match") 3))
       ((equal token "|") (if (smie-rule-parent-p "with") 3))
       ((equal token ":=")
-       (if (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive")
+       (if (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive"
+                               "Function")
            (or proof-indent smie-indent-basic)))))))
 
 ;;
@@ -821,7 +862,9 @@ This is specific to `coq-mode'."
         proof-script-imenu-generic-expression coq-generic-expression)
 
   (if (and coq-use-smie (fboundp 'smie-setup))
-      (smie-setup coq-smie-grammar #'coq-smie-rules)
+      (smie-setup coq-smie-grammar #'coq-smie-rules
+                  :forward-token #'coq-smie-forward-token
+                  :backward-token #'coq-smie-backward-token)
     (require 'coq-indent)
     (setq
      ;; indentation is implemented in coq-indent.el