diff options
Diffstat (limited to 'generic')
| -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) |