Fix bug with nested spans, solving #344/#335

2 files changed, 24 insertions, 9 deletions

diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index cdf69a1b..18c0db81 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -33,6 +33,21 @@
   (pg-autotest remark "Testing standard Example.thy, Example-Xsym.thy")
   (pg-autotest script-wholefile "isar/Example.thy")
 
+  ;; Test Trac#344 (nested spans bug with old-style undo)
+  ;; TODO: should test with both undo styles
+  (pg-autotest eval (proof-retract-buffer))
+  (proof-shell-wait)
+  (goto-char 135) ; first line
+  (pg-autotest eval (proof-goto-point))
+  (proof-shell-wait)
+  (pg-autotest eval (proof-retract-buffer))
+  (proof-shell-wait)
+  (goto-char 135) ; first line
+  (pg-autotest eval (proof-goto-point))
+  (proof-shell-wait)
+  (pg-autotest eval (proof-process-buffer))
+  (pg-autotest assert-full)
+
   ;; Speed up prover
   (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
   (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
@@ -63,7 +78,7 @@
   (pg-autotest script-wholefile "isar/Example-Tokens.thy")
 
   (pg-autotest remark "Testing random jumps and edits")
-  (pg-autotest script-randomjumps "isar/Example.thy" 5)
+  (pg-autotest script-randomjumps "isar/Example.thy" 8)
 
   (when isar-long-tests
       (pg-autotest remark "Larger files...")
diff --git a/isar/isar.el b/isar/isar.el
index 1afbc66e..6a4e05a1 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -436,30 +436,30 @@ This is called when Proof General spots output matching
 (defun isar-find-and-forget (span)
   "Return commands to be used to forget SPAN."
   (let (str ans answers)
-    (while (and span (span-property span 'cmd))
-      (setq str (or (span-property span 'cmd) ""))
+    (while span
+      (setq str (span-property span 'cmd))
       (setq ans nil)
       (cond
        ;; comment, diagnostic, nested proof command: skip
        ;; FIXME: should adjust proof-nesting-depth here.
        ((or (eq (span-property span 'type) 'comment)
 	    (eq (span-property span 'type) 'proverproc)
-	    (eq (span-property span 'type) 'proof); da: needed?
-	    (proof-string-match isar-undo-skip-regexp str)
-	    (proof-string-match isar-undo-ignore-regexp str)))
+	    (eq (span-property span 'type) 'proof)
+	    (and str (proof-string-match isar-undo-skip-regexp str))
+	    (and str (proof-string-match isar-undo-ignore-regexp str))))
        ;; finished goal: undo
        ((eq (span-property span 'type) 'goalsave)
 	(setq ans isar-undo))
        ;; open goal: skip and exit
-       ((proof-string-match isar-goal-command-regexp str)
+       ((and str (proof-string-match isar-goal-command-regexp str))
 	(setq span nil))
        ;; control command: cannot undo
-       ((and (proof-string-match isar-undo-fail-regexp str))
+       ((and str (proof-string-match isar-undo-fail-regexp str))
 	(setq ans (isar-cannot-undo (match-string 1 str)))
 	(setq answers nil)
 	(setq span nil))
        ;; theory: remove and exit
-       ((proof-string-match isar-undo-remove-regexp str)
+       ((and str (proof-string-match isar-undo-remove-regexp str))
 	(setq ans (isar-remove (match-string 3 str)))
 	(setq span nil))
        ;; else: undo