branch: elpa/proof-general
commit 921c23daac6109069655363f685e808a88b4f211
Author: Pierre Courtieu <[email protected]>
Commit: Pierre Courtieu <[email protected]>
Plugging back coq-indent-proofstart and coq-indent-modulestart.
Was removed in the refactoring of indentation some weeks ago.
---
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 b3357d0651..b74d38b879 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1307,7 +1307,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)))
@@ -1375,6 +1374,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)
