diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-01-14 16:45:39 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-01-14 16:45:39 +0000 |
| commit | 8846ae205897eb04673f093d7e1e13d9da7af6ae (patch) | |
| tree | 9f92e38faf638dfe4c2131880d063d32fa80f136 /coq/coq-smie.el | |
| parent | 351eae29f2da9644cae5ba1fc3a1c36d7bf9c803 (diff) | |
changed default indentation of match's cases.
Diffstat (limited to 'coq/coq-smie.el')
| -rw-r--r-- | coq/coq-smie.el | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 66e4fbe1..993674b6 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -639,6 +639,18 @@ Lemma foo: forall n, :type 'boolean :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. +For example the default value 2 makes indetation like this: + +match n with + O => ... +| S n => ... +end + +Typical values are 2 or 4." + :type 'integer :group 'coq) ;; - TODO: remove tokens "{ subproof" and "} subproof" but they are ;; needed by the lexers at a lot of places. @@ -702,7 +714,7 @@ Lemma foo: forall n, (moduledecl) (moduledef) (exp)) - (commands (commands "." commands) + (commands (commands "." commands) (commands "- bullet" commands) (commands "+ bullet" commands) (commands "* bullet" commands) @@ -815,7 +827,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." "with module" "as" ":= inductive" ":= module" ))) 2) - ((equal token "with match") 4) + ((equal token "with match") coq-match-indent) ((equal token "; tactic") (cond |