diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 15:24:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 15:24:50 +0000 |
| commit | 9caefd6216b544d22aa927fb8a07a1a925491536 (patch) | |
| tree | cd20c6956eb558375fa6c6508bdcd8ab9bc85bbf /isar | |
| parent | 78969186e204e14daa05f7662a2d3d223cd5466c (diff) | |
Work on Trac #335 (broken old style script management)
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 7 |
1 files changed, 2 insertions, 5 deletions
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 |