From a88b79a4e42bbb2e12e290c46496e3dde162de95 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 4 Jul 2006 17:10:27 +0000
Subject: 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).

---
 coq/coq-indent.el | 15 ++++++++++-----
 1 file 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)))))
-- 
cgit v1.2.3