From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Mon, 25 May 2020 10:55:03 +0200 Subject: fix: backtrack wrong type argument --- generic/proof-shell.el | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'generic/proof-shell.el') 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) -- cgit v1.2.3