diff options
| author | Anaclet | 2020-05-25 10:55:03 +0200 |
|---|---|---|
| committer | Anaclet | 2020-05-29 11:05:58 +0200 |
| commit | 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 (patch) | |
| tree | 32d6e1a6407bc18c62685233229ad6c74cb6d64b /generic/proof-shell.el | |
| parent | 411ebb27fda4d39fc22baf341dcdde2341632b8d (diff) | |
fix: backtrack wrong type argument
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1258c7f6..9e51d4fb 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1181,21 +1181,23 @@ 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) - (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 - (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) + (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) |