fix issue ProofGeneral#605

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.
@@ -98,6 +155,9 @@ so the response buffer should not be cleared."
   ;; window.  Indicate it should be erased before the next output.
   (pg-response-maybe-erase t t nil keepresponse)
 
+  ;; ;; commit modif
+  ;; (reset-goals-modeline)
+
   ;; Erase the goals buffer and add in the new string
   (with-current-buffer proof-goals-buffer
 
@@ -106,13 +166,15 @@ so the response buffer should not be cleared."
     (unless (eq 0 (buffer-size))
       (bufhist-checkpoint-and-erase))
 
-    ;; Only display if string is non-empty.
-    (unless (string-equal string "")
-      (funcall pg-insert-text-function string))
+    ;; Display the string only if it's non-empty.
+    ;; In that case, parse and update goals information in 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)
-    
+
     ;; Keep point at the start of the buffer.
     (proof-display-and-keep-buffer
      proof-goals-buffer (point-min))))

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)
 	      )

generic/proof-shell.el

@@ -870,7 +870,8 @@ after a completed proof."
     (proof-shell-exec-loop))
 
    ((proof-re-search-forward-safe proof-shell-proof-completed-regexp end t)
-    (setq proof-shell-proof-completed 0))) ; commands since complete
+    (setq proof-shell-proof-completed 0)))
+   ;; (reset-goals-modeline))) ; commands since complete
 
   ;; PG4.0 change: simplify and run earlier
   (if proof-shell-handle-output-system-specific
@@ -1788,7 +1789,10 @@ i.e., 'goals or 'response."
 			gmark))
 	    (rstart start)		 ; possible response before goals
 	    (gend   end)
-	    both)			 ; flag for response+goals
+	    both
+            (proof-termination-regexp
+             (concat "\\(" coq-proof-end-regexp "\\|"
+                     coq-definition-end-regexp "\\)"))) ;flag for response+goals
 
        (goto-char gstart)
        (while (re-search-forward proof-shell-start-goals-regexp end t)

generic/proof-tree.el

@@ -407,7 +407,6 @@ a proof. Therefore, if non-nil, this variable must either hold a
 nonempty list (the to be delayed action items) or t (if there are
 no action items to be delayed.")
 
-
 ;;; Missing in the library
 
 (defun list-pred-partition (p l)
@@ -422,7 +421,8 @@ that takes one argument."
       (if (funcall p x)
           (push x yes)
         (push x no)))))
-
+
+
 ;;
 ;; process filter function that receives prooftree output
 ;;
@@ -894,7 +894,6 @@ current buffer."
 	(list sequent-id sequent-text additional-goal-ids))
     nil))
 
-
 (defun proof-tree-extract-existential-info (start end)
   "Extract the information display of existential variables.
 This function cuts out the text between
@@ -982,7 +981,6 @@ The delayed output of the navigation command is in the region
 	  ;; send all to prooftree
 	  (proof-tree-send-switch-goal proof-state proof-name current-id)))))
 
-
 (defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info)
   "Display current goal in prooftree unless CMD should be ignored."
   ;; (message "PTHPC")
@@ -998,7 +996,7 @@ The delayed output of the navigation command is in the region
 	(proof-tree-handle-proof-progress old-proof-marker
 					  cmd-string proof-info)))
     (setq proof-tree-last-state (car proof-info))))
-    
+
 (defun proof-tree-handle-undo (proof-info)
   "Undo prooftree to current state."
   ;; (message "PTHU info %s" proof-info)
@@ -1016,7 +1014,6 @@ The delayed output of the navigation command is in the region
 	(proof-tree-send-undo proof-state))
     (setq proof-tree-last-state proof-state)))
 
-
 (defun proof-tree-update-sequent (proof-name)
   "Prepare an update-sequent command for prooftree.
 This function processes delayed output that the proof assistant
@@ -1072,6 +1069,20 @@ the flags and SPAN is the span."
   (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags))
     (let* ((proof-info (funcall proof-tree-get-proof-info))
 	   (current-proof-name (cadr proof-info)))
+
+;; commit first issue
+      (save-excursion
+        (goto-char proof-shell-delayed-output-start)
+        (when (re-search-forward proof-tree-current-goal-regexp proof-shell-delayed-output-end t)
+          (let ((goal (match-string-no-properties 1))
+                (id (match-string-no-properties 2))
+                (shelved (match-string-no-properties 3)))
+            ;; Now call the update function with extracted information
+            (update-goals-modeline goal id shelved))))
+
+;;
+
+
       (save-excursion
 	(if (< (car proof-info) proof-tree-last-state)
 	    ;; went back to some old state: there must have been an undo command