focus rocq goal buffer on the top of the iris goal

iris.el

;; modified from coq-show-first-goal in proof-general-20251120.1746/coq/coq.el
(defun iris-show-first-goal ()
  "Scroll the goal buffer so that the first goal is visible.
First goal is displayed on the bottom of its window, maximizing the
number of hypothesis displayed, without hiding the goal"
  (interactive)
  ;; CPC 2015-12-31: Added the check below: if the command that caused this
  ;; call was silent, we shouldn't touch the goals buffer.  See GitHub issues
  ;; https://github.com/cpitclaudel/company-coq/issues/32 and
  ;; https://github.com/cpitclaudel/company-coq/issues/8.
  (unless (memq 'no-goals-display proof-shell-delayed-output-flags)
    (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting the good frame
      (with-selected-frame (or pg-frame (window-frame (selected-window)))
        ;; prefer current frame
        (let ((goal-win (or (get-buffer-window proof-goals-buffer) (get-buffer-window proof-goals-buffer t))))
          (if goal-win
              (with-selected-window goal-win
                ;; find snd goal or buffer end, if not found this goes to the
                ;; end of buffer
                (search-forward-regexp "\\(?:sub\\)?goal 2\\|\\*\\*\\* Unfocused goals:\\|\\'")
                (beginning-of-line)
                ;; find something backward else than a space: bottom of concl
                (ignore-errors (search-backward-regexp "\\S-"))
                (recenter (- 1)) ; put bot of concl at bottom of window
                (beginning-of-line)
                ;; if the top of concl is hidden we may want to show it instead
                ;; of bottom of concl
                (when coq-prefer-top-of-conclusion
                  (let* ((iris-proof-mode-start
                          (save-excursion
                            (re-search-backward "--------------------------------------[□∗]" nil t)))
                         (goal-start (save-excursion (re-search-backward "========" nil t)))
                         (ipm-p (and iris-proof-mode-start goal-start
                                     (< goal-start iris-proof-mode-start))))

                    ;; is the proof mode active?
                    (if ipm-p
                        (progn
                          (when (not (<= (window-start) iris-proof-mode-start))
                            (goto-char iris-proof-mode-start)
                            (recenter) ;0
                            (beginning-of-line)))

                      ;; we're not in proof mode, behave like coq-show-first-goal
                      ;; return nil if === is not visible
                      (if (and goal-start (not (<= (window-start) goal-start)))
                          (progn (goto-char goal-start)
                                 (recenter) ;0
                                 (beginning-of-line))
                        (unless goal-start
                          (goto-char (point-min))))))))))))))

(remove-hook 'proof-shell-handle-delayed-output-hook 'coq-show-first-goal)
(add-hook 'proof-shell-handle-delayed-output-hook 'iris-show-first-goal)
(setq coq-prefer-top-of-conclusion t)