Coq indentation small fixes.

1 files changed, 113 insertions, 96 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index a96cc1a0..79e98b1e 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -108,46 +108,52 @@ detect if they start something or not."
 (defconst coq-end-command-regexp 
   "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\(\\.\\)\\(?:\\s-\\|\\'\\)")
 
+(defun coq-looking-at-syntactic-context ()
+  (or (proof-looking-at-syntactic-context)
+      (when (not (eq (point) (point-min)))
+        (save-excursion 
+          (forward-char -1)
+          (when (proof-looking-at-safe proof-script-comment-start-regexp) 'comment)))))
 
 (defun coq-find-command-end-backward ()
-  "Moves to the first end of command found looking up.  The point is put exactly before the last \".\" of the ending token.  If no end command is found, go as far as possible and return nil."
-  (if (string-match coq-end-command-regexp (buffer-substring (point-min) (point)))
-      (progn 
-        (proof-re-search-backward coq-end-command-regexp)
-        (goto-char (match-beginning 1)))
-    (goto-char (point-min))
-    nil))
+  "Moves to the first end of command found looking up.  The point is put exactly
+before the last \".\" of the ending token.  If no end command is found, go as far as
+possible and return nil."
+  (forward-char 1); because regexp looks one char after last "."
+  (when (proof-re-search-backward coq-end-command-regexp nil 'dummy)
+    (goto-char (match-beginning 1))))
 
 (defun coq-find-command-end-forward ()
-  "Moves to the first end of command found looking up.  The point is put exactly before the last \".\" of the ending token.  If no end command is found, go as far as possible and return nil."
-  (if (string-match coq-end-command-regexp (buffer-substring (point) (point-max)))
-      (progn
-        (proof-re-search-forward coq-end-command-regexp)
-        (goto-char (match-beginning 1)))
-    (goto-char (point-max))
-    nil))
+  "Moves to the first end of command found looking down.  The point is put exactly
+before the last \".\" of the ending token.  If no end command is found, go as far as
+possible and return nil."
+;  (if (string-match coq-end-command-regexp (buffer-substring (point) (point-max)))
+  (when (proof-re-search-forward coq-end-command-regexp nil 'dummy)
+    (goto-char (match-beginning 1))))
 
 
 (defun coq-find-command-end (direction)
-  "Moves to the first end of command found looking at direction.  The point is put exactly before the last \".\" of the ending token.  If no end command is found, go as far as possible and return nil."
-  (if (< direction 0)
-      (coq-find-command-end-backward)
+  "Moves to the first end of command found looking at direction.  The point is put
+exactly before the last \".\" of the ending token.  If no end command is found, go as
+far as possible and return nil."
+  (if (< direction 0) (coq-find-command-end-backward)
     (coq-find-command-end-forward)))
 
-
-
-(defun coq-find-command-start-backward ()
-  "Move to the start of current command."
+(defun coq-find-current-start ()
+  "Move to the start of command at point.
+The point is put exactly after the end of previous command, or at the (point-min if
+there is no previous command)."
   (coq-find-command-end-backward)
   (while (and (proof-looking-at-syntactic-context)
 				  (> (point) (point-min)))
     (coq-find-command-end-backward))
   (if (proof-looking-at "\\.\\s-") (forward-char 1))
-  (point)
-  )
+  (point))
 
 (defun coq-find-real-start ()
-  (coq-find-command-start-backward)
+  "Move to the start of command at point.
+The point is put exactly before first non comment letter of the command."
+  (coq-find-current-start)
   (proof-re-search-forward "\\w\\|\\s(\\|\\s)\\|\\'")
   (backward-char 1)
   (while (and (proof-looking-at-syntactic-context)
@@ -155,27 +161,14 @@ detect if they start something or not."
     (proof-re-search-forward "\\*\\s)");this does not deal with nested comments
     (proof-re-search-forward "\\w\\|\\s(\\|\\s)\\|\\'")
     (backward-char 1))
-  (point)
-  )
+  (point))
 
-(defun coq-find-end ()
-  (coq-find-command-end-forward)
-  (if (= (point) (+ (match-beginning 0) 2)) (backward-char 1))
-  (while (and (proof-looking-at-syntactic-context)
-				  (<= (point) (point-max)))
-    (proof-re-search-forward "\\*\\s)")
-    (proof-re-search-forward coq-end-command-regexp)
-    (if (= (point) (+ (match-beginning 0) 2)) (backward-char 1)))
-  (point)
-  )
-
-(defun coq-current-command-string ()
+(defun coq-command-at-point ()
+  "Return the string of the command at point."
   (save-excursion
     (let ((st (coq-find-real-start)) ; va chercher trop loin?
-          (nd (coq-find-command-end-forward))) ; idem?
-      (buffer-substring st (+ nd 1)))
-    )
-  )
+          (nd (or (coq-find-command-end-forward) (- (point-max) 1)))) ; idem?
+      (buffer-substring st (+ nd 1)))))
 
 (defun is-at-a-space-or-tab ()
   "t si le caractere courant est un blanc ou un tab, nil sinon"
@@ -191,48 +184,69 @@ detect if they start something or not."
 )
 
 (defun find-reg (lim reg)
-  "Return non nil if there is an occurrence of reg between point and lim which is not a comment or a string.  Actually returns the position of the occurrence found.  Point is not moved"
+  "Return non nil if there is an occurrence of reg between point and lim which is not
+a comment or a string.  Actually returns the position of the occurrence found.  Point
+is moved at the end of the match if found, at LIM otherwise."
   (let ((oldpt (point)) (limit lim))
-    (if (= limit (point)) nil)
-    ;;swap limit and point if necessary
-    (if (< limit (point)) (let ((x limit)) (setq limit (point)) (goto-char x)))
-    (let ((pos nil))
-      (while 
-          (and (not pos)
-               (setq pos (proof-string-match reg (buffer-substring (point) limit))))
-        (forward-char pos)
-        (if (proof-looking-at-syntactic-context) (progn (setq pos nil) (forward-char 1)))
-        )
-      (and pos (point)))
-    )
-  )
+    (if (= limit (point)) nil
+      ;;swap limit and point if necessary
+      (message "find-reg...")
+      (when (< limit (point)) (let ((x limit)) (setq limit (point)) (goto-char x)))
+      (let ((pos nil))
+        (while 
+            (and (not pos)
+                 (setq pos (proof-string-match reg (buffer-substring (point) limit))))
+          (message "while body...")
+          (forward-char (- (match-end 0) 1))          
+          (when (save-excursion (forward-char -1)
+                                (proof-looking-at-syntactic-context))
+            (setq pos nil))
+          (message "while body... done"))
+        (message "find-reg... after while")
+        (and pos (point))))))
+
+
+(defun coq-find-no-syntactic-on-line ()
+  (let ((bol (save-excursion (beginning-of-line) (point)))
+        (eol (save-excursion (end-of-line) (point))))
+    (beginning-of-line)
+    (back-to-indentation)
+    (while (and (or (coq-looking-at-syntactic-context)
+                    (is-at-a-space-or-tab))
+                    (not (eq (point) eol)))
+      (forward-char 1))
+    (not (eq (point) eol))))
 
 (defun coq-back-to-indentation-prevline ()
   "Moves point back to previous pertinent line for indentation. Move point to the first non white space character. Returns 0 if top of buffer was reached, 3 if inside a comment or string, 4 if inside the {} of a record, 1 if the line found is not in the same command as the point before the function was called, 2 otherwise (point and previous line are in the same command, and not inside the {} of a record)."
   (if (proof-looking-at-syntactic-context) 3
     (let ((oldpt (point))
-          (topnotreached (= (forward-line -1) 0))) ; nil if going one line backward
-                                        ; is not possible
+          (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward
+                                                   ;;; is not possible
+      
       (while (and topnotreached
-                  (or (only-spaces-on-line) (proof-looking-at-syntactic-context))
-                  t;;(> (line-number (point)) (line-number (point-min)))
+                  (not (coq-find-no-syntactic-on-line))
+                  t ;;(> (line-number (point)) (line-number (point-min)))
                   )
         (setq topnotreached (= (forward-line -1) 0)))
       (back-to-indentation)
-      (if (not topnotreached) 0;; returns nil if top of buffer was reached
+      (message "coq-back-to-indentation-prevline... after while")
+      (if (not topnotreached) 0 ;; returns nil if top of buffer was reached
         ;; if we are at end of a command (dot) find this command
-        (if (find-reg oldpt coq-end-command-regexp) (progn (coq-find-real-start) 1)
+        (if (find-reg oldpt coq-end-command-regexp) 
+            (progn (forward-char -2)
+                   (message "coq-back-to-indentation-prevline... coq-find-real-start")
+                   (coq-find-real-start)
+                   (message "coq-back-to-indentation-prevline... coq-find-real-start2")
+                   1)
           (if (save-excursion 
-                (and (coq-find-real-start)
+                (message "coq-back-to-indentation-prevline... if 3")
+                (and (or (forward-char -1) t)
+                     (coq-find-real-start)
                      (proof-looking-at-safe "Record")
                      (find-reg oldpt "{"))) 
               4 
-            2))
-		  
-        )
-      )
-    )
-  )
+            2))))))
 
 
 (defun coq-find-unclosed (&optional optlvl limit openreg closereg)
@@ -381,34 +395,35 @@ detect if they start something or not."
   "Returns the indentation offset of the current line. This function indents a *command* line (the first line of a command). Use `coq-indent-expr-offset' to indent a line belonging to an expression."
   (cond
 
-	((proof-looking-at-safe "\\<Proof\\>") 0) ; no indentation at "Proof ..."
+   ((proof-looking-at-safe "\\<Proof\\>") 0);; no indentation at "Proof ..."
 
-  ; we are at an end command -> one ident left
-  ; FIX: we should count the number of closing item on the line
-	((coq-save-command-p nil (coq-current-command-string)) 
-	 (- proof-indent))
+   ;; we are at an end command -> one ident left
+   ;; FIX: we should count the number of closing item on the line
+   ((coq-save-command-p (or (coq-command-at-point) "")) 
+    (- proof-indent))
 
 
-  ; previous command is a goal command -> one indent right
-  ; carreful: this line moves the point
-	((and (goto-char prevpoint) 
-			(or (and ;"Proof ..." is a proof start (but not really a goal command)
-                  ;  unless followed by a term (catch by coq-save-command-p above
-				  (proof-looking-at-safe "\\<Proof\\>")
-				  (not (coq-save-command-p nil (coq-current-command-string))))
-				 (coq-indent-goal-command-p (coq-current-command-string))))
-	 proof-indent)
+   ;; previous command is a goal command -> one indent right
+   ;; carreful: this line moves the point
+   ((and (goto-char prevpoint)
+         (or (and;;"Proof ..." is a proof start (but not really a goal command)
+              ;;  unless followed by a term (catch by coq-save-command-p above
+              (proof-looking-at-safe "\\<Proof\\>")
+              (not (coq-save-command-p (coq-command-at-point))))
+             (coq-indent-goal-command-p (coq-command-at-point))
+             ))
+    proof-indent)
 
-;	((and (goto-char prevpoint) 
-;         ;"Proof <term>." is actually a Save command
-;         ; catched only if not follwed by"." or "with"
-;			(proof-looking-at-safe "\\<Proof\\>"))
-;	 (- proof-indent))
+;;	((and (goto-char prevpoint) 
+;;         ;"Proof <term>." is actually a Save command
+;;         ; catched only if not follwed by"." or "with"
+;;			(proof-looking-at-safe "\\<Proof\\>"))
+;;	 (- proof-indent))
 
 
-  ; otherwise -> same indent as previous command
-	(t 0)
-	)
+   ;; otherwise -> same indent as previous command
+   (t 0)
+   )
   )
 
 
@@ -546,9 +561,10 @@ argument must be t if inside the {}s of a record, nil otherwise."
       (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)) ())
+        (let ((eol (save-excursion (end-of-line) (point))))
         (if (and (not atstart)
                  (string-match coq-comment-start-regexp 
-                               (buffer-substring (point) (line-end-position))))
+                               (buffer-substring (point) eol)))
             (progn (proof-re-search-forward coq-comment-start-regexp) (forward-char 1))
           (if (and (not atstart) (proof-looking-at-syntactic-context))
               (progn (proof-re-search-forward "\\S-")
@@ -556,7 +572,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
             ;;we are at the first line of a comment
             (goto-char oldpt)
             (coq-find-command-end-backward)
-            (coq-find-real-start)))
+            (coq-find-real-start))))
         (current-column)))))
 
 
@@ -566,14 +582,15 @@ argument must be t if inside the {}s of a record, nil otherwise."
 		(setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
 				prevcol (current-column)
 				prevpoint (point)))
+   (message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint)
 	 (cond 
 	  ((= kind 0) 0) ; top of the buffer reached
 	  ((= kind 1) ; we are at the command level
-		(+ prevcol (coq-indent-command-offset kind prevcol prevpoint)))
+     (+ prevcol (coq-indent-command-offset kind prevcol prevpoint)))
 	  ((= kind 2) ; we are at the expression level
-		(coq-indent-expr-offset kind prevcol prevpoint nil))
+     (coq-indent-expr-offset kind prevcol prevpoint nil))
 	  ((= kind 4) ; we are at the expression level inside {}s of a record
-		(coq-indent-expr-offset kind prevcol prevpoint t))
+     (coq-indent-expr-offset kind prevcol prevpoint t))
 	  ((= kind 3) (coq-indent-comment-offset)))))
 
 (defun coq-indent-calculate ()