From e88df8ab52c1fbe90b2f88b2b52b3ff7b3a1f9c2 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 28 May 2020 14:25:33 +0200 Subject: [PATCH] Show command sent only once and only in proof mode. --- generic/proof-shell.el | 37 +++++++++++++++++++++++++++++++------ 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9a5784a90..192855ae4 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1101,7 +1101,6 @@ processed without calling this function." "Add item to `proof-priority-action-list' and start the queue if necessary. Argument QUEUEITEM must be an action item as documented for `proof-action-list'." - (message "PATPQ") (push queueitem proof-priority-action-list) (start-prover-with-priority-items-maybe)) @@ -1661,14 +1660,40 @@ by the filter is to send the next command from the queue." (buffer-substring-no-properties start end)) ;; sets proof-shell-last-output-kind + ;;; NB This will remove the span (and all following queued spans) + ;;; if an error occured. So don't use it in the following unless + ;;; you know the command was processed without error. (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)))) + ;; in case of error. Currently PG makes coq silent when proccesing + ;; a bunch of commands, and goes back to unsilent before the last + ;; command. Therefore if an error interrupts a bunch we are still + ;; in silent mode and the goal is not diplayed. The following + ;; inserts a show proof command to have an up-to-date goals buffer + ;; in case of error AND we are in a proof. We don't issue the show + ;; command in other cases as it would be redundant or wrong. + + ;; NB: If we switch to "all silent, ask for show" protocol, then + ;; this would need to be generalized, but maybe not here. + + ;; NB: To avoid looping on errors (like if the printing of the + ;; goal is not possible) these actions are tagged with the flag + ;; 'empty-action-list and trigger the following only if its this + ;; flag is missing. + (when (and (not (memq 'empty-action-list flags)) + (funcall proof-shell-last-cmd-left-goals-p) + (eq proof-shell-last-output-kind 'error)) + ;; to make the error message stay, we need to send a Show + ;; command without updating any buffer and then use the + ;; pg-goals-display can insert the output in goals buffer + ;; without changing the response buffer. + (let ((callback '(lambda (dummyspan);do not use the span, it is probably deleted + (pg-goals-display proof-shell-last-output t)))) + (proof-add-to-priority-queue + (proof-shell-action-list-item + proof-showproof-command callback ;'proof-done-invisible + (list 'no-goals-display 'invisible 'empty-action-list))))) (unless proof-shell-last-output-kind ; dealt with already (setq proof-shell-delayed-output-start start)