Experimental fix for #220.

2 files changed, 53 insertions, 10 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 878fb895..95b982ef 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -104,13 +104,19 @@ detect if they start something or not."
 
 No context checking.")
 
+;; Goal selector syntax
+(defconst coq-goal-selector-regexp "[0-9]+\\s-*:\\s-*")
+
 ;; We can detect precisely bullets (and curlies) by looking at there
 ;; prefix: the prefix should be a real "." then spaces then only
 ;; bullets and curlys and spaces). This is used when search backward.
 ;; This variable is the regexp of possible prefixes
 (defconst coq-bullet-prefix-regexp
   (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp "\\)"
-          "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)"))
+          "\\(?:\\.\\)\\(?:\\s-\\)"
+          "\\(?:\\s-\\|"
+          "\\(?:" coq-goal-selector-regexp "\\)?"
+          "{\\|}\\|-\\|+\\|\\*\\)*\\)"))
 
 ;; matches regular command end (. and ... followed by a space or buffer end)
 ;; ". " and "... " are command endings, ".. " is not, same as in
@@ -152,7 +158,9 @@ There are 2 substrings:
 * number 2 is the left context matched that is not part of the bullet"  )
 
 (defconst coq-curlybracket-end-command
-  "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)"
+  (concat "\\(?:\\(?1:"
+          "\\(?:" coq-bullet-prefix-regexp"\\)?"
+          "{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)")
   "Matches ltac curlies when searching backward. Warning: False positive.
 
 There are 3 substrings (2 and 3 may be nil):
@@ -165,7 +173,10 @@ This matches more than real ltac curlies. See
 only when searching backward).")
 
 (defconst coq-curlybracket-end-command-backward
-  (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)")
+  (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)"
+          "\\(?:\\(?:\\(?1:" "\\(?:" coq-goal-selector-regexp "\\)?{\\)"
+          "\\(?3:[^|]\\)\\)"
+          "\\|\\(?1:}\\)\\)\\)")
   "Matches ltac curly brackets when searching backward.
 
 This should match EXACTLY script structuring curlies. No false
@@ -357,8 +368,21 @@ Comments are ignored, of course."
         (start (coq-find-not-in-comment-backward "[^[:space:]]")))
     ;; we must find a "." to be sure, because {O} {P} is allowed in definitions
     ;; with implicits --> this function is recursive
-    (if (looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p)
-      (looking-at "\\.\\|\\`"))))
+    (cond
+     ;; "{" can be prefixed by a goal selector (coq-8.8).
+     ;; TODO: looking-back is supposed to be slow. Find something else? 
+     ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t))
+          (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t))
+          (and (looking-at "[0-9]+:\\s-*{") nil t))
+      (goto-char (match-beginning 0)); swallow goal selector
+      (coq-empty-command-p))
+     ;; other bulleting syntax
+     ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p))
+     ;; not a bullet, we foound something else, it shoulf be either a
+     ;; dot or the beginning of the file, otherwise we are in the
+     ;; middle of a command
+     (t (looking-at "\\.\\|\\`"))
+     )))
 
 
 ; slight modification of proof-script-generic-parse-cmdend (one of the
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 11952b68..4565d86c 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -586,12 +586,28 @@ The point should be at the beginning of the command name."
       (goto-char (1- (point))) "{|")
 
      ((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
-	   (save-excursion
-	     (forward-char -1)
-	     (let ((nxttok (coq-smie-backward-token))) ;; recursive call
-	       (coq-is-cmdend-token nxttok))))
+           (save-excursion
+             (forward-char -1)
+             (if (and (looking-at "{")
+                      (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
+                 (goto-char (match-beginning 0)))
+             (let ((nxttok (coq-smie-backward-token))) ;; recursive call
+               (coq-is-cmdend-token nxttok))))
       (forward-char -1)
-      (if (looking-at "{") "{ subproof" "} subproof"))
+      (if (looking-at "}") "} subproof"
+        (if (and (looking-at "{")
+                 (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
+            (goto-char (match-beginning 0)))
+        "{ subproof"
+        ))
+
+     ;; ((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
+     ;;       (save-excursion
+     ;;         (forward-char -1)
+     ;;         (let ((nxttok (coq-smie-backward-token))) ;; recursive call
+     ;;           (coq-is-cmdend-token nxttok))))
+     ;;  (forward-char -1)
+     ;;  (if (looking-at "{") "{ subproof" "} subproof"))
 
      ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
       ": ltacconstr")
@@ -618,6 +634,9 @@ The point should be at the beginning of the command name."
      ((member tok '("*;" "-*;" "|-*;" "*|-*;"))
       ;; FIXME; can be "; ltac" too
       (forward-char (- (length tok) 1)) "; tactic")
+     ;; bullet detected, is it really a bullet? we have to traverse
+     ;; recursively any other bullet or "n:{" "}". this is the work of
+     ;; coq-empty-command-p
      ((and (string-match coq-bullet-regexp-nospace tok)
 	   (save-excursion (coq-empty-command-p)))
       (concat tok " bullet"))