aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2018-01-26 14:39:26 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2018-01-26 14:39:26 -0500
commitd672652f4acb78b83403b080665e6c56e00f4feb (patch)
tree7d3182309bd1f3a07504b2a628ad662f9cc3f73e
parent8762209b3b7aeeaee52d11624eef2a676392c72a (diff)
look for vernac controls before focus bracket, fix for #223
-rw-r--r--coq/coq-indent.el9
1 files changed, 8 insertions, 1 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 95b982ef..b6b8c18d 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -378,7 +378,14 @@ Comments are ignored, of course."
(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
+ ;; vernacular controls Time, Fail, Redirect, Timeout
+ ((or (and (looking-at "e\\>") (looking-back "\\<Tim") (- (point) 3))
+ (and (looking-at "l\\>") (looking-back "\\<Fai") (- (point) 3))
+ (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+"))
+ (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*")))
+ (goto-char (match-beginning 0))
+ (coq-empty-command-p))
+ ;; not a bullet, we found something else, it should be either a
;; dot or the beginning of the file, otherwise we are in the
;; middle of a command
(t (looking-at "\\.\\|\\`"))