From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Thu, 28 May 2020 09:21:53 +0200 Subject: [PATCH] fix: backtrack for "Show Proof" disabled --- coq/coq.el | 44 +++++++++++++++++++++++++++++------------- generic/proof-shell.el | 43 ++++++++++++++++++++--------------------- 2 files changed, 52 insertions(+), 35 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 9fc6e2005..df7c5a668 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1220,12 +1220,17 @@ should match the `coq-show-proof-diffs-regexp'." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (list "Show." - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (let ((showlist (list "Show."))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")) + "Show Proof.") + t)) + showlist)) ((or ;; If we go back in the buffer and the number of abort is less than @@ -1233,12 +1238,23 @@ should match the `coq-show-proof-diffs-regexp'." (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") + ;; (when coq-show-proof-stepwise + ;; (or + ;; (when (eq coq-diffs 'off) "Show Proof.") + ;; (when (eq coq-diffs 'on) "Show Proof Diffs.") + ;; (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs." ) + (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")) + "Show Proof.") + t)) + showlist)) ((or ;; If we go back in the buffer and not in the above case, then only Unset @@ -1254,10 +1270,12 @@ should match the `coq-show-proof-diffs-regexp'." (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0))) (when coq-show-proof-stepwise + (if (coq--post-v811) (or (when (eq coq-diffs 'off) (list "Show Proof." )) (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))) + (list "Show Proof.")))))) (defpacustom auto-adapt-printing-width t diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9e51d4fb3..b9ac2b3cf 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization." (not (memq 'empty-action-list flags)) proof-shell-empty-action-list-command) (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) - (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) - ;; tag all new items with 'empty-action-list - (extra-items (mapcar (lambda (s) (proof-shell-action-list-item - s 'proof-done-invisible - (list 'invisible 'empty-action-list))) - extra-cmds))) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) ;; action-list should be empty at this point (setq proof-action-list (append extra-items proof-action-list)))) @@ -1181,23 +1181,22 @@ contains only invisible elements for Prooftree synchronization." ;; process the delayed callbacks now (mapc 'proof-shell-invoke-callback cbitems) - (unless (or proof-action-list proof-second-action-list-active) + (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup - (proof-release-lock) - (proof-detach-queue) - (unless flags ; hint after a batch of scripting - (pg-processing-complete-hint)) - (pg-finish-tracing-display)) - - - (and (not proof-second-action-list-active) - (let ((last-command (car (nth 1 (car (last proof-action-list)))))) - (or (null proof-action-list) - (cl-every - (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list) - ;; If the last command in proof-action-list is a "Show Proof" form then return t - (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) + (proof-release-lock) + (proof-detach-queue) + (unless flags ; hint after a batch of scripting + (pg-processing-complete-hint)) + (pg-finish-tracing-display)) + + (and (not proof-second-action-list-active) + (let ((last-command (car (nth 1 (car (last proof-action-list)))))) + (or (null proof-action-list) + (cl-every + (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) + proof-action-list) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd)