From 9caefd6216b544d22aa927fb8a07a1a925491536 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 18 Aug 2010 15:24:50 +0000 Subject: Work on Trac #335 (broken old style script management) --- isar/isar.el | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'isar') diff --git a/isar/isar.el b/isar/isar.el index b4150b98..606824c9 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -441,14 +441,11 @@ 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 span + (while (and span (span-property span 'cmd)) (setq str (or (span-property span 'cmd) "")) (setq ans nil) (cond ;; comment, diagnostic, nested proof command: skip - ;; (da: adding new span types may break this code, - ;; ought to test for type 'cmd before looking at - ;; str below) ;; FIXME: should adjust proof-nesting-depth here. ((or (eq (span-property span 'type) 'comment) (eq (span-property span 'type) 'proverproc) @@ -468,7 +465,7 @@ This is called when Proof General spots output matching (setq span nil)) ;; theory: remove and exit ((proof-string-match isar-undo-remove-regexp str) - (setq ans (isar-remove (match-string 2 str))) + (setq ans (isar-remove (match-string 3 str))) (setq span nil)) ;; else: undo (t -- cgit v1.2.3