diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2006-07-04 17:10:27 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2006-07-04 17:10:27 +0000 |
commit | a88b79a4e42bbb2e12e290c46496e3dde162de95 (patch) | |
tree | 75db69041b6a216ef9168c038c6b46b0ef9e8f10 /coq/coq-indent.el | |
parent | dafc82fac00976f0caaaad43d66778759b93827d (diff) |
fix the bug for coq indetation of two consecutive comments. Code is
ugly, should take the code given by Stefan Monnier and adapt it (it
does not indent everything as is).
Diffstat (limited to 'coq/coq-indent.el')
-rw-r--r-- | coq/coq-indent.el | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index afcbf161..f7cac5d8 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -187,7 +187,7 @@ detect if they start something or not." ) (defun only-spaces-on-line () - "t if there is only spaces (or nothing) on the current line after point" + "t if there is only spaces (or nothing) on the current line after point. Moves point to first non space char if present." (while (and (char-after) (is-at-a-space-or-tab)) (forward-char 1)) (if (or (not (char-after)) (char-equal (char-after) ?\n)) t nil) @@ -552,16 +552,21 @@ argument must be t if inside the {}s of a record, nil otherwise." (defun coq-indent-comment-offset () (save-excursion - (let ((oldpt (point))) + (let ((oldpt (point)) + ;; atstart is true if the line to indent is a comment start + (atstart (proof-looking-at coq-comment-start-regexp))) (if (/= (forward-line -1) 0) 0 ; we are at beginning of buffer + ;; only-space on a non empty line moves the point to first non space char (while (and (only-spaces-on-line) (= (forward-line -1) 0)) ()) - (if (string-match coq-comment-start-regexp - (buffer-substring (point) (line-end-position))) + (if (and (not atstart) + (string-match coq-comment-start-regexp + (buffer-substring (point) (line-end-position)))) (progn (proof-re-search-forward coq-comment-start-regexp) (forward-char 1)) - (if (proof-looking-at-syntactic-context) + (if (and (not atstart) (proof-looking-at-syntactic-context)) (progn (proof-re-search-forward "\\S-") (goto-char (match-beginning 0))) ;;we are at the first line of a comment + (goto-char oldpt) (coq-find-command-end-backward) (coq-find-real-start))) (current-column))))) |