Fixed indentation and goal display.

3 files changed, 20 insertions, 19 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index baa46836..6bd41349 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -111,16 +111,17 @@ Return nil if not found."
 (defun coq-skip-until-one-comment-backward ()
   "Skips comments and normal text until finding an unclosed comment start.
 Return nil if not found.  Point is moved to the the unclosed comment start
-if found, to (point-max) otherwise."
-  (ignore-errors (backward-char 1))       ; if point is between '(' and '*'
-  (if (looking-at coq-comment-start-regexp) t
-    (forward-char 1)
-    (let ((nbopen 1) (kind nil))
-      (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward)))
-        (if (< kind 0)
-            (setq nbopen (+ 1 nbopen))
-          (setq nbopen (- nbopen 1))))
-      (= nbopen 0))))
+if found, to (point-max) otherwise. return true if found, nil otherwise."
+  (if (= (point) (point-min)) nil
+    (ignore-errors (backward-char 1))       ; if point is between '(' and '*'
+    (if (looking-at coq-comment-start-regexp) t
+      (forward-char 1)
+      (let ((nbopen 1) (kind nil))
+        (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward)))
+          (if (< kind 0)
+              (setq nbopen (+ 1 nbopen))
+            (setq nbopen (- nbopen 1))))
+        (= nbopen 0)))))
 
 (defun coq-skip-until-one-comment-forward ()
   "Skips comments and normal text until finding an unopened comment end."
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index ec17d506..ad51d990 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -844,7 +844,7 @@ Used by `coq-goal-command-p'"
   "Keywords for tacticals in a Coq script.")
 
 
-                                        ; From JF Monin:
+ ;; From JF Monin:
 (defvar coq-reserved
   (append 
    coq-user-reserved-db
diff --git a/coq/coq.el b/coq/coq.el
index 9f507412..295fdf6a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1566,18 +1566,17 @@ First goal is displayed on the bottom of its window, maximizing the
 number of hypothesis displayed, without hiding the goal"
   (interactive)
   (let* ((curwin (selected-window))
-	 (goalbuf (get-buffer-window proof-goals-buffer)))
+         (goalbuf (get-buffer-window proof-goals-buffer)))
     (if (eq goalbuf nil) ()
       (select-window goalbuf)
       (search-forward-regexp "subgoal 2\\|\\'"); find snd goal or buffer end
-      (recenter (- (window-height) 1))	; scroll 
+      (beginning-of-line)
+      (ignore-errors (search-backward-regexp "\\S-")) ; find something else than a space
+      (recenter (- 1)) ; put it at bottom og window
       (let ((msg (concat (first-word-of-buffer) " subgoals")))
-	(select-window curwin)		; go back to current window
-	(message msg)                   ; display the number of goals
-	)
-      )
-    )
-  )
+        (select-window curwin)
+        (message msg)                   ; display the number of goals
+        ))))
 
 ;; This hook must be added before optim-resp-window, in order to be evaluated
 ;; *after* windows resizing.
@@ -1618,6 +1617,7 @@ Only when three-buffer-mode is enabled."
       )))
 
 ;; TODO: I would rather have a response-insert-hook thant this two hooks
+;; Careful: optim-resp-windows must be called AFTER proof-show-first-goal
 ;; Adapt when displaying a normal message
 (add-hook 'proof-shell-handle-delayed-output-hook 'optim-resp-windows)
 ;; Adapt when displaying an error or interrupt