branch: elpa/proof-general
commit 1f93bf273d3e7f8e371671cbab58f9fbb8c5f68a
Merge: a967f22805 dd9c8a2b67
Author: Pierre Courtieu <mata...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #788 from Matafou/fix-debug-mode
Fixing the debug mode (for recent coq verions).
Lain problem was that intermediate goals during debug steps was not
dispatched to goals bugger anymore. This patch fixes that.
---
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 5790004843..c66b8107a9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1317,8 +1317,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 496fc2a538..d12382d4a2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1841,23 +1841,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)))
@@ -2004,7 +2010,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.
