Fix #29 + indentation glitch + regexp refactoring.

1 files changed, 79 insertions, 40 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 406fc673..fddfc373 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -96,77 +96,116 @@ detect if they start something or not."
                (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str)))))))
 
 
+(defconst coq-simple-cmd-ender-regexp "[^.]\\|\\=\\|\\.\\."
+  "Used internally. Matches the allow prefix of the coq \".\" command ending.")
+
+(defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+"
+  "Matches single bullet, WARNING: Lots of false positive.
+
+No context checking.")
+
+;; 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-regexp "\\)"
+          "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)"))
+
 ;; matches regular command end (. and ... followed by a space or buffer end)
 ;; ". " and "... " are command endings, ".. " is not, same as in
 ;; proof-script-command-end-regexp in coq.el
 (defconst coq-period-end-command
-  "\\(?:\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)")
+  (concat "\\(?:\\(?2:" coq-simple-cmd-ender-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)")
+  "Matches coq regular syntax for ending a command (except bullets and curlies).
 
-;; matches curly bracket but not {| and |} WARNING this matches more
-;; than the script parenthesizing '{' and '}' as curly bracket may
-;; match this when used in regular expressions
-(defconst coq-curlybracket-end-command
-  "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)")
+This should match EXACTLY command ending syntax. No false
+positive should be accepted. \"...\" is matched as \".\" with a
+left context \"..\".
 
-
-
-;; bullets must be preceded by a space but since we usually
-;; search for this expression from the first non white char of the
-;; command, so we give two versions of this regexp
-
-;; matches bullets. WARNING this matches more than real bullets as - +
-;; and * may match this when used in regular expressions
-;(defconst coq-bullet-end-command
-;  "\\(?2:\\s-\\|\\=\\)\\(?:\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)\\)")
-;; Allowing - -- --- and + ++ +++ ...
+There are 3 substrings (2 and 3 may be nil):
+* number 1 is the real bullet string,
+* number 2 is the left context matched that is not part of the bullet
+* number 3 is the right context matched that is not part of the bullet
+")
 
 ;; captures a lot of false bullets, need to check that the commaand is
 ;; empty. When searching forward (typically when splitting the buffer
 ;; into commands commands) we can't do better than that.
-;; For backward searching see `coq-bullet-end-command-backward' below.
 (defconst coq-bullet-end-command
-   "\\(?:\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)")
+  (concat "\\(?:\\(?2:\\s-\\|\\=\\)" "\\(?1:" coq-bullet-regexp-nospace "\\)\\)")
+  "Matches ltac bullets. WARNING: lots of false positive.
 
-(defconst coq-bullet-regexp-nospace
-  "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)")
+This matches more than real bullets as - + and * may match this
+when used in regular expressions. See
+`coq-bullet-end-command-backward' for a more precise regexp (but
+only when searching backward).")
 
-;; Trying to capture precisely bullets when search backward (forward
-;; is harder since we need to look backward if a dot is eventually
-;; there)
+;; Context aware detecting regexp, usefull when search backward.
 (defconst coq-bullet-end-command-backward
-"\\(?:\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)"
-)
+  (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)")
+  "Matches ltac bullets when searching backward.
+
+This should match EXACTLY bullets. No false positive should be accepted.
+There are 2 substrings:
+* number 1 is the real bullet string,
+* number 2 is the left context matched that is not part of the bullet"  )
+
+(defconst coq-curlybracket-end-command
+  "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)"
+  "Matches ltac curlies when searching backward. Warning: False positive.
+
+There are 3 substrings (2 and 3 may be nil):
+* number 1 is the real bullet string,
+* number 2 is the left context matched that is not part of the bullet
+* number 3 is the right context matched that is not part of the bullet
+
+This matches more than real ltac curlies. See
+`coq-bullet-end-command-backward' for a more precise regexp (but
+only when searching backward).")
+
+(defconst coq-curlybracket-end-command-backward
+  (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)")
+  "Matches ltac curly brackets when searching backward.
+
+This should match EXACTLY script structuring curlies. No false
+positive should be accepted.
+There are 3 substrings (2 and 3 may be nil):
+* number 1 is the real bullet string,
+* number 2 is the left context matched that is not part of the bullet
+* number 3 is the right context matched that is not part of the bullet")
 
-;; order matter here, since bullet regexp contains period regexp
 (defconst coq-end-command-regexp
   (concat coq-period-end-command "\\|"
           coq-bullet-end-command "\\|"
           coq-curlybracket-end-command)
-;  "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)"
-  "Regexp matching end of a command. There are 3 substrings:
+  "Matches end of commands (and ltac bullets and curlies). WARNING: False positive.
+
+There are 3 substrings:
 * number 1 is the real coq ending string,
 * number 2 is the left context matched that is not part of the ending string
 * number 3 is the right context matched that is not part of the ending string
 
-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.
-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.")
+WARNING: this regexp accepts some curly brackets and bullets (+ -
+*) with no sufficient context verification. Lots of false
+positive are matched. Currently bullets and curlies 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 in
+coq-smie.el, and see `coq-end-command-regexp-backward' for a more
+precise regexp (but only when searching backward).")
 
 (defconst coq-end-command-regexp-backward
   (concat coq-bullet-end-command-backward "\\|"
           coq-period-end-command "\\|"
-          coq-curlybracket-end-command)
-;  "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)"
-  "Regexp matching end of a command. There are 3 substrings:
+          coq-curlybracket-end-command-backward)
+  "Matches end of commands, including bullets and curlies.
+
+There are 3 substrings (2 and 3 may be nil):
 * number 1 is the real coq ending string,
 * number 2 is the left context matched that is not part of the ending string
 * number 3 is the right context matched that is not part of the ending string
 
-This regexp is much more precise than `coq-end-command-regexp' but only
+Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only
 works when searching backward.")