From 8846ae205897eb04673f093d7e1e13d9da7af6ae Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 14 Jan 2015 16:45:39 +0000 Subject: changed default indentation of match's cases. --- coq/coq-smie.el | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'coq/coq-smie.el') 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 -- cgit v1.2.3