From 9d71e253eeca2c4fe9e687a517c796699267f1e0 Mon Sep 17 00:00:00 2001
From: Axel Daboust <axel.daboust@telecom-paris.fr>
Date: Sun, 7 Apr 2024 16:19:46 +0200
Subject: [PATCH] fix issue #605

---
 generic/pg-goals.el     | 62 +++++++++++++++++++++++++++++++++++++++--
 generic/proof-script.el |  1 +
 2 files changed, 61 insertions(+), 2 deletions(-)

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index f7cb9b3c7..9626cf194 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -79,6 +79,63 @@ May enable proof-by-pointing or similar features.
 ;;
 ;; Goals buffer processing
 ;;
+
+;; update *goals* buffer modeline
+(defun coq-parse-goals-info (goals-output)
+  "Parse output to extract and update goals information in modeline."
+  (let ((goals-count-regexp "^\\([0-9]+\\) goals? (ID \\([0-9]+\\))")
+        (num-goals 0)
+        (current-goal-id nil))
+    (when (string-match goals-count-regexp goals-output)
+      (setq num-goals (string-to-number (match-string 1 goals-output)))
+      (setq current-goal-id (match-string 2 goals-output)))
+    (update-goals-modeline num-goals current-goal-id)
+    ; hide goals info on first line
+    (with-current-buffer proof-goals-buffer
+      (goto-char (point-min))
+      (let ((line-end (line-end-position)))
+        (let ((overlay (make-overlay (point-min) line-end)))
+          ; invisible line
+          (overlay-put overlay 'invisible t))))))
+
+(defun update-goals-modeline (goal id)
+  "Extracts proof state and updates the goals buffer modeline dynamically."
+  (with-current-buffer proof-goals-buffer
+    (let ((goal-str (if (> goal 1) "goals" "goal")))
+      (setq-local my-goals-info
+                  (format "%d %s, ID: %s" goal goal-str id)))
+      (let ((baseline-mode-line-format
+             '("%e"
+               mode-line-front-space
+               mode-line-mule-info
+               mode-line-client
+               mode-line-modified
+               mode-line-remote
+               mode-line-frame-identification
+               mode-line-buffer-identification
+               " "
+               mode-line-position
+               " "
+               mode-line-modes
+               mode-line-misc-info
+               mode-line-end-spaces)))
+
+        (setq-local mode-line-format
+                    (append baseline-mode-line-format
+                            `((" " (:eval my-goals-info))))) ; update
+
+        (force-mode-line-update))))
+
+(defun reset-goals-modeline ()
+  "Resets the *goals* buffer modeline to indicate no active proof."
+  (with-current-buffer proof-goals-buffer
+    (setq-local my-goals-info "")
+    (setq-local mode-line-format
+                (append
+                 '("%e" mode-line-front-space mode-line-mule-info mode-line-client mode-line-modified mode-line-remote mode-line-frame-identification mode-line-buffer-identification " " mode-line-position " " mode-line-modes mode-line-misc-info mode-line-end-spaces)
+                 `((" " (:eval my-goals-info)))))
+    (force-mode-line-update)))
+
 (defun pg-goals-display (string keepresponse)
   "Display STRING in the `proof-goals-buffer', properly marked up.
 Converts term substructure markup into mouse-highlighted extents.
@@ -107,8 +164,9 @@ so the response buffer should not be cleared."
       (bufhist-checkpoint-and-erase))
 
     ;; Only display if string is non-empty.
-    (unless (string-equal string "")
-      (funcall pg-insert-text-function string))
+    (when (not (string-equal string ""))
+      (funcall pg-insert-text-function string)
+      (coq-parse-goals-info string))
 
     (setq buffer-read-only t)
     (set-buffer-modified-p nil)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 854bd6bf8..07212e060 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1486,6 +1486,7 @@ Besides stuff that is not yet documented here, this function
   and sections.
 - enters some commands and their spans in some database (with for
   me unknown purpose)"
+  (reset-goals-modeline) ; Erase goal buffer when a proof is closed
   (unless (or (eq proof-shell-proof-completed 1)
 	      ;; (eq proof-assistant-symbol 'isar)
 	      )