From c29f373a57dbc88dcdd47f110ce1d65b91fbb38f Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 6 Jun 2012 15:54:37 +0000
Subject: Fixing a bug with the indentation of qualified names.

---
 coq/coq.el | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 9ad31e15..96ad2db0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -440,31 +440,40 @@ Lemma foo: forall n,
   "Parsing table for Coq.  See `smie-grammar'.")
 
 (defun coq-smie-search-token-forward (tokens &optional end)
-  "Search for one of TOKENS between point and END."
+  "Search for one of TOKENS between point and END.
+Token \".\" is considered only if followed by a space."
   (unless end (setq end (point-max)))
   (condition-case nil
       (catch 'found
         (while (< (point) end)
           ;; The default lexer is faster and is good enough for our needs.
           (let ((next (smie-default-forward-token)))
-            (cond
-             ((zerop (length next)) (forward-sexp 1))
-             ((member next tokens) (throw 'found next))))))
+            ;; 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)
-  "Search for one of TOKENS between point and END."
+  "Search for one of TOKENS between point and END.
+Token \".\" is considered only if followed by a space."
   (unless end (setq end (point-min)))
   (condition-case nil
       (catch 'found
         (while (> (point) end)
           ;; The default lexer is faster and is good enough for our needs.
           (let ((next (smie-default-backward-token)))
-            (cond
-             ((zerop (length next)) (forward-sexp -1))
-             ((member next tokens) (throw 'found next))))))
+            ;; 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)))
 
+
 ;; Lexer.
 ;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence
 ;;   constraint ":= < | < ; < :=" where ":= < |" is due to Inductive
-- 
cgit v1.2.3