Fixed the cleaning of goals buffer when proof completed

+ fixed the refreshing of modeline goal number display.

2 files changed, 8 insertions, 9 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 7a0238fd..32e76015 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -268,16 +268,9 @@ The point is put exactly before first non comment letter of the command."
           (nd (or (coq-find-command-end-forward) (- (point-max) 1)))) ; idem?
       (if st (buffer-substring st (+ nd 1))))))
 
-(defun coq-ident-line-number (pt)
- (save-excursion
-   (goto-char pt)
-   (if (= 0 (current-column)) (+ (line-number pt) 1)
-     (line-number pt))
-   )
- )
 
 (defun same-line (pt pt2)
- (or (= (coq-ident-line-number pt) (coq-ident-line-number pt2))))
+ (or (= (line-number-at-pos pt) (line-number-at-pos pt2))))
 
 (defun coq-commands-at-line ()
   "Return the string of each command at current line.."
@@ -346,7 +339,6 @@ not inside the {} of a record)."
                                                    ;;; is not possible
       (while (and topnotreached
                   (not (coq-find-no-syntactic-on-line))
-                  ;(> (line-number (point)) (line-number (point-min)))
                   )
         (setq topnotreached (= (forward-line -1) 0))
         (end-of-line)
diff --git a/coq/coq.el b/coq/coq.el
index 4530efb2..5e9f14e6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -362,6 +362,7 @@ If locked span already has a state number, then do nothing. Also updates
 ;; commands is started
 (add-hook 'proof-state-change-hook 'coq-set-state-infos)
 
+
 (defun count-not-intersection (l notin)
   "Return the number of elts of L that are not in NOTIN."
   (let ((l1 l) (l2 notin) (res 0))
@@ -741,6 +742,7 @@ This is specific to `coq-mode'."
   (setq
    proof-shell-cd-cmd coq-shell-cd
    proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\""   . "\\\""))
+   proof-shell-clear-goals-regexp coq-shell-proof-completed-regexp
    proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
    proof-shell-error-regexp coq-error-regexp
    proof-shell-interrupt-regexp coq-interrupt-regexp
@@ -1404,6 +1406,11 @@ number of hypothesis displayed, without hiding the goal"
 	  'coq-show-first-goal)
 (add-hook 'proof-shell-handle-delayed-output-hook
 	  'coq-update-minor-mode-alist)
+(add-hook 'proof-shell-handle-delayed-output-hook
+          '(lambda () 
+             (if (proof-string-match coq-shell-proof-completed-regexp
+                                     proof-shell-last-output)
+                 (proof-clean-buffer proof-goals-buffer))))
 
 
 (defun is-not-split-vertic (selected-window)