From 3fd4d7ed1495c139cd575f300dfc4c4937959156 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 11 Mar 2020 21:27:55 +0100 Subject: [PATCH] insert show proof command on error --- generic/proof-shell.el | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 0c5ccbde2..172ba0a0b 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1663,6 +1663,13 @@ by the filter is to send the next command from the queue." ;; sets proof-shell-last-output-kind (proof-shell-handle-immediate-output cmd start end flags) + ;; insert a show proof command to have an up-to-date goals buffer + ;; in case of error + (when (eq proof-shell-last-output-kind 'error) + (proof-add-to-priority-queue + (proof-shell-action-list-item + proof-showproof-command 'proof-done-invisible (list 'invisible)))) + (unless proof-shell-last-output-kind ; dealt with already (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end)