diff options
| -rw-r--r-- | CHANGES | 25 | ||||
| -rw-r--r-- | coq/coq-smie.el | 16 |
2 files changed, 32 insertions, 9 deletions
@@ -47,16 +47,27 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Default indentation of forall and exists is not boxed anymore For instance, this is now indented like this: - Lemma foo: forall x y, - x = 0 -> ... . (* like if forall x y, was on its own line *) - + Lemma foo: forall x y, + x = 0 -> ... . instead of: - - Lemma foo: forall x y, - x = 0 -> ... . - + Lemma foo: forall x y, + x = 0 -> ... . do this: (setq coq-indent-box-style t) to bring the box style back. +*** Default indentation cases of "match with" are now indented by 2 instead of 4. + "|" is indented by zero: + + match n with + 0 => ... + | S n => ... + end + instead of: + match n with + 0 => ... + | S n => ... + end + do this: (setq coq-match-indent 4) to bring old behaviour back. + *** Support for bullets, braces and Grab Existential Variables for Prooftree. *** Support for _Coqproject files 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 |