diff options
| author | Pierre Courtieu | 2015-01-27 09:27:09 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2015-01-27 09:27:09 +0000 |
| commit | 2af210aeab374b6fcd55db2a155d897a17face0b (patch) | |
| tree | d39af26f307278d99653ea0b645017a3dad2d6fb | |
| parent | 8846ae205897eb04673f093d7e1e13d9da7af6ae (diff) | |
Fixed a bug in script navigation. Updated CHANGE
| -rw-r--r-- | CHANGES | 13 | ||||
| -rw-r--r-- | coq/coq-indent.el | 4 |
2 files changed, 16 insertions, 1 deletions
@@ -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)) |