insert show proof command on error

ProofGeneral · Mar 11, 2020 · cd3dba8 · cd3dba8
1 parent 58bacd1
commit cd3dba8
Showing 1 changed file with 7 additions and 0 deletions.
diff --git 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)