fixed a bug in command parsing for coq, due to recent changes.

3 files changed, 23 insertions, 21 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index c842400f..fc229d6e 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -133,7 +133,10 @@ detect if they start something or not."
 WARNING: this regexp accepts curly brackets (if not preceded by
 '|') and bullets (+ - *) (if preceded by a space or at cursor).
 This is of course not correct and some more check is needed to
-distinguish between the different uses of this characters. This is done below and also in coq-smie.el.")
+distinguish between the different uses of this characters.
+Currently bullets are always ending an empty command, so we just
+need to check that the command ended by the bullet-like regexp is empty.
+This is done below and also in coq-smie.el.")
 
 
 (defun coq-search-comment-delimiter-forward ()
@@ -309,11 +312,16 @@ command end regexp."
                          (match-end 1)))
                   (setq next-pos (+ 1 (match-beginning 0)))
                   (or
-                      (if (or (string-equal (match-string 1) "}")
-                              (string-equal (match-string 1) "{")
-                              (string-equal (match-string 1) "-")
-                              (string-equal (match-string 1) "+")
-                              (string-equal (match-string 1) "*"))
+                      (if (not (or (string-equal (match-string 1) ".")
+                                   (string-equal (match-string 1) "...")))
+                          ; command-end that are not a dot are + ++ -
+                          ; -- etc or { or } to ensure this is really
+                          ; a bullet (and not one of the numerous
+                          ; other possible uses of those tokens) we
+                          ; check that the command ended by it is
+                          ; empty. example:
+                          ; destruct x.
+                          ; - (* - here ends an empty command*)
                           (save-excursion
                             (goto-char (match-beginning 1))
                             (not (coq-empty-command-p)))
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 52e1aa39..3d2d421c 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -478,8 +478,7 @@ The point should be at the beginning of the command name."
 	   (save-excursion
 	     (forward-char -1)
 	     (let ((nxttok (coq-smie-backward-token))) ;; recursive call
-	       (coq-is-cmdend-token nxttok)
-	       )))
+	       (coq-is-cmdend-token nxttok))))
       (forward-char -1)
       (if (looking-at "{") "{ subproof" "} subproof"))
 
@@ -505,14 +504,9 @@ The point should be at the beginning of the command name."
      ; for "unfold in *|-*;"
      ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic")
      ((and (string-match coq-bullet-regexp-nospace tok)
-	   (save-excursion
-	     (let ((prev (coq-smie-backward-token))) ;; recursive call
-	       (or (coq-is-subproof-token prev)
-		   (coq-is-dot-token prev)))))
+	   (save-excursion (coq-empty-command-p)))
       (concat tok " bullet"))
 
-
-
      ((and (member tok '("exists" "∃"))
 	   (save-excursion
 	     ;; recursive call looking at the ptoken immediately before
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 7218fa63..6644df83 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -15,22 +15,22 @@ Record a : Type := make_a {
   | C2 : forall n, test n
   | C3 : forall n, test n
   | C4 : forall n, test n.
-
+  
   Inductive test2 : nat -> Prop
     := C1 : forall n, test n
      | C2 : forall n, test n
      | C3 : forall n, test n
      | C4 : forall n, test n.
-
+  
   Let x : = 1.  Let y := 2.
-                
+  
   Let y := (1, 2, 3,
             4, 5).
   
-    Inductive test3             (* fixindent *)
-      : nat -> Prop
-      := C1 : forall n, test n
-       | C2 : forall n, test n
+  Inductive test3             (* fixindent *)
+    : nat -> Prop
+    := C1 : forall n, test n
+     | C2 : forall n, test n
 }
 
 Lemma toto:nat.