diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-01-06 17:24:28 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-01-06 17:24:28 +0100 |
| commit | 4558ea05882f4b207d1de0224a04aa995d423701 (patch) | |
| tree | ab3326e0ddf181a86f0dbfeb7a3ea60ee3cc69d1 /coq/coq-smie.el | |
| parent | a326ff399be1691643fe4bbbde4a27896b194e82 (diff) | |
Adding uset preference coq-indent-semicolon-tactical.
Some people prefer ";" tactical to be non indented, in particular in
Ltac definitions. Setting this variable to 0 (2 by default) does it. You
can still have some indentation by putting ; at beginning of lines:
tac1
; tac2
; tac3.
Diffstat (limited to 'coq/coq-smie.el')
| -rw-r--r-- | coq/coq-smie.el | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 939e0cc3..ab825ec8 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -687,6 +687,23 @@ Lemma foo: forall n, :type 'integer :group 'coq) +(defcustom coq-indent-semicolon-tactical 2 + "Number of spaces used to indent after the first tactical semi colon of a serie. + If set to 0, indetation is as follows: + tac1; + tac2; + tac3; + tac4. + + if set to 2 (default): + + tac1; + tac2; + tac3; + tac4." + :type 'integer + :group 'coq) + (defcustom coq-indent-modulestart 2 "Number of spaces used to indent after a module or section start." :type 'integer @@ -905,7 +922,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "; tactic") (cond ((smie-rule-parent-p "; tactic") (smie-rule-separator kind)) - (t (smie-rule-parent 2)))) + (t (smie-rule-parent coq-indent-semicolon-tactical)))) ; "as" tactical is not idented correctly ((equal token "in let") (smie-rule-parent)) |