diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | coq/coq-smie.el | 17 |
2 files changed, 25 insertions, 0 deletions
@@ -36,6 +36,14 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** smie indentation is now the only choice. Old code removed. will work only if emacs >= 23.3. +*** indentation off modules, sections and proofs are customizable + + (setq coq-indent-modulestart X) will set indentation width for + modules and sections to X characters + + (setq coq-indent-proofstart X) will set indentation width for + modules and sections to X characters + *** indentation of match with cases: by default the indentation is like this now: match n with diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 9a7df711..06cc2582 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -639,6 +639,16 @@ Lemma foo: forall n, :type 'boolean :group 'coq) +(defcustom coq-indent-proofstart 2 + "Number of spaces used to indent after a proof start." + :type 'integer + :group 'coq) + +(defcustom coq-indent-modulestart 2 + "Number of spaces used to indent after a module or section start." + :type 'integer + :group 'coq) + (defcustom coq-match-indent 2 "Number of space used to indent cases of a match expression. If the \"|\" separator is used, indentation will be reduced by 2. @@ -838,6 +848,13 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "in let") (smie-rule-parent)) ((equal token "} subproof") (smie-rule-parent)) + + ; using user customized variable to set indentation of modules, + ; section and proofs. + ((equal token ". proofstart") + (smie-rule-parent coq-indent-proofstart)) + ((equal token ". modulestart") + (smie-rule-parent coq-indent-modulestart)) )) (:before |