diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-03-09 17:16:58 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-09 17:16:58 +0000 |
| commit | 0d2fd4c7e2b76ff868648ed1f6d51c9e5bc6bbf0 (patch) | |
| tree | 1d0322d91c2478c408570d9f132d627f2d9e86f1 /generic | |
| parent | bbcee39f5bf8eb74445d4abb78a7aac2ad048cb5 (diff) | |
Fixes #503.
Added a "stop silent" if needed in proof-add-queue. This allows to
recover verbosity when an error left the prover in silent mode.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b0ae9684..69af75f5 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -925,6 +925,15 @@ track what happens in the proof queue." ;; More efficient: keep track of size of queue as modified. (>= (length proof-action-list) proof-shell-silent-threshold))) +(defsubst proof-shell-should-not-be-silent () + "Non-nil if we should switch to non silent mode based on size of queue." + (if (and proof-shell-stop-silent-cmd ; configured + proof-shell-silent) ; already non silent + ;; NB: to be more accurate we should only count number + ;; of scripting items in the list (not e.g. invisibles). + ;; More efficient: keep track of size of queue as modified. + (< (length proof-action-list) proof-shell-silent-threshold))) + (defsubst proof-shell-insert-action-item (item) "Insert ITEM from `proof-action-list' into the proof shell." @@ -975,7 +984,7 @@ being processed." (if proof-action-list ;; something to do (progn - (if (proof-shell-should-be-silent) + (when (proof-shell-should-be-silent) ;; do this ASAP, either first or just after current command (setq proof-action-list (if nothingthere ; the first thing @@ -984,6 +993,17 @@ being processed." (cons (car proof-action-list) ; after current (cons (proof-shell-start-silent-item) (cdr proof-action-list)))))) + ;; Sometimes the non silent mode needs to be set because a + ;; previous error prevented to go back to non silent mode + (when (proof-shell-should-not-be-silent) + ;; do this ASAP, either first or just after current command + (setq proof-action-list + (if nothingthere ; the first thing + (cons (proof-shell-stop-silent-item) + proof-action-list) + (cons (car proof-action-list) ; after current + (cons (proof-shell-stop-silent-item) + (cdr proof-action-list)))))) (when nothingthere ; start sending commands (proof-grab-lock queuemode) (setq proof-shell-last-output-kind nil) |