From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 09:21:53 +0200
Subject: fix: backtrack for "Show Proof" disabled

---
 generic/proof-shell.el | 43 +++++++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 22 deletions(-)

(limited to 'generic')

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)
-- 
cgit v1.2.3