From 084d783ff4f6f1c622011b75ae5fd25bbe6cbf7d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Mon, 9 Sep 2024 18:01:35 +0200
Subject: [PATCH] Fixing the debug mode (for recent coq verions).

Coq stopped printing <infomsg></infomsg> around debug infos some
versions ago. This has been preventing response and goals buffers to
dispatch debug info. This patch seems fixes.
---
 coq/coq-syntax.el |  3 ++-
 coq/coq.el        | 32 ++++++++++++++++++++------------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a3e7f3ab0..7d3251d6f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1316,8 +1316,9 @@ Very similar to `coq-omit-proof-admit-command', but without the dot."
 ;; april2017: coq-8.7 removes special chars definitely and puts
 ;; <infomsg> and <warning> around all messages except errors.
 ;; We let our legacy regexp for some years and remove them, say, in 2020.
+;; 09/2024: Adding more eager annotations to fix debug mode.
 (defvar coq-shell-eager-annotation-start
-   "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>\\|<warning>")
+   "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>\\|<warning>\\|Going to execute:")
 
 (defvar coq-shell-eager-annotation-end
   "\377\\|done\\]\\|</infomsg>\\|</warning>\\|\\*\\*\\*\\*\\*\\*\\|) >")
diff --git a/coq/coq.el b/coq/coq.el
index 4eb493810..98291f113 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1837,23 +1837,29 @@ at `proof-assistant-settings-cmds' evaluation time.")
 (defun coq-display-debug-goal ()
   (interactive)
   (with-current-buffer proof-shell-buffer
-    (let ((pt (progn (save-excursion (forward-line -1) (point)))))
+    (goto-char (point-max))
+    (let ((pt (save-excursion (forward-line -1) (point)))
+          (last-prompt (save-excursion (forward-line -1)
+                                       (re-search-backward "</prompt>" nil t))))
       (save-excursion
-        (re-search-backward "^TcDebug" pt t)
-        (re-search-backward "<infomsg>\\|^TcDebug\\|^</prompt>" nil t)
-        (when (looking-at "<infomsg>")
-          (let ((pt2 (point)))
-            (re-search-backward "Goal:\\|^TcDebug\\|^</prompt>" nil t)
-            (when (looking-at "Goal")
-              (pg-goals-display (buffer-substring (point) pt2) nil))))))))
+        (when (and
+               (re-search-backward "^TcDebug" pt t) ;; current TcDebug
+               (re-search-backward "^TcDebug" last-prompt t)) ;; previous one
+               (re-search-forward "^Goal:" pt t))
+        (beginning-of-line)
+        (let ((pt2 (point)))
+          (re-search-forward "</prompt>\\|^Debug:\\|^Going to execute:\\|^TcDebug" nil t)
+          (goto-char (match-beginning 0))
+          (pg-goals-display (buffer-substring pt2 (point)) nil)
+          (beginning-of-line)
+          (pg-response-message (buffer-substring (point) (point-max)))
+          )))))
 
 ;; overwrite the generic one, interactive prompt is Debug mode;; try to display
 ;; the debug goal in the goals buffer.
 (defun proof-shell-process-interactive-prompt-regexp ()
   "Action taken when `proof-shell-interactive-prompt-regexp' is observed."
-  (when (and (proof-shell-live-buffer)
-	     ; not already visible
-	     t)
+  (when (proof-shell-live-buffer)
     (switch-to-buffer proof-shell-buffer)
     (coq-display-debug-goal)
     (message "Prover expects input in %s buffer (if debug mode: h<return> for help))" proof-shell-buffer)))
@@ -2001,7 +2007,9 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-shell-eager-annotation-start coq-shell-eager-annotation-start
    proof-shell-eager-annotation-start-length 32
 
-   proof-shell-interactive-prompt-regexp "TcDebug "
+   ;; we need these two strings to be recognized so that the first appearing is
+   ;; analyzed
+   proof-shell-interactive-prompt-regexp "TcDebug ([0-9]+) >\\|Going to execute:"
 
    ;; ****** is added at the end of warnings in emacs mode, this is temporary I
    ;;        want xml like tags, and I want them removed before warning display.