diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 43 |
1 files changed, 21 insertions, 22 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9e51d4fb..b9ac2b3c 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) |