branch: elpa/proof-general
commit 40c40d229e9db177f2114266ac6246daf6a060bc
Merge: f34a493839 921c23daac
Author: Pierre Courtieu <mata...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #617 from Matafou/fix-indent-user-prefs
Fix indent user prefs
---
coq/coq-smie.el | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 00c1fd5e38..5d6c4fccda 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1308,7 +1308,6 @@ If nil, default to `proof-indent' if it exists or to
`smie-indent-basic'."
((member tk '("with" ":" "by" "in tactic" "as" ",")) "tactic infix")
((member tk '("<:" "<+" "with module")) "modulespec infix") ;; ":=
inductive" ":= module" and other ":= xxx"
((string-prefix-p ":= " tk) "after :=")
- ((member tk '(". proofstart" ". modulestart")) "dot script parent open")
;; by default we pass the token name, but maybe it would be safer
;; to simply fail, so that we detect missing tokens in this function?
(t tk)))
@@ -1376,6 +1375,8 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
(`(:after . ,_) ;; indent relative to token (parent of token at point).
(pcase (coq-indent-categorize-token-after token)
("} subproof" 0) ;;shouldn't be captured by (:elem . args)?
+ (". proofstart" coq-indent-proofstart)
+ (". modulestart" coq-indent-modulestart)
;; decrement indentation when hanging
((and (or "tactic infix" "after :=") (guard (or (hang-p)
(smie-rule-bolp)))) 0)
((and "->" (guard (hang-p))) 0) ((or ":=" "with inductive") 2)
