aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES13
-rw-r--r--coq/coq-indent.el4
2 files changed, 16 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 8ac72cf9..a99ca5cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,19 @@ 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 of match with cases:
+ by default the indentation is like this now:
+ match n with
+ O => ...
+ | S n => ...
+ end
+ do this: (setq coq-match-indent 4) to get back the
+ previous indetation style:
+ match n with
+ O => ...
+ | S n => ...
+ end
+
*** indentation now supports { at end of line:
example:
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index da73f808..93feebca 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -391,7 +391,9 @@ and return nil."
The point is put exactly after the end of previous command, or at the (point-min if
there is no previous command)."
(coq-script-parse-cmdend-backward)
- (if (proof-looking-at "\\.\\s-\\|{\\|}") (forward-char 1)) ; else = no match found
+ (when
+ (proof-looking-at "\\.\\s-\\|{\\|}\\|\\++\\|\\*+\\|-+")
+ (forward-char (- (match-end 0) (match-beginning 0)))) ; else = no match found
(point))