[nongnu] elpa/proof-general 921c23daac 1/2: Plugging back coq-indent-proofstart and coq-indent-modulestart.

[ELPA Syncer]

branch: elpa/proof-general
commit 921c23daac6109069655363f685e808a88b4f211
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    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)