diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-06-05 14:00:41 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-06-05 14:00:41 +0000 |
| commit | 8a300d77dab9e8985a8de3050861c1f20bbd7b67 (patch) | |
| tree | 404c05399a18c350878c020f2214ba5b6c19b676 /isar | |
| parent | 8ddfe310072fb9ba46cca11a3a52b45f1d9a94a2 (diff) | |
Temporary bug fix to solve nil span error message
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/isar/isar.el b/isar/isar.el index 83c601a3..ca40baa8 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -464,19 +464,22 @@ proof-shell-retract-files-regexp." (let ((ans nil) (lev 0) cmd) (while (and span (not ans)) (setq span (prev-span span 'type)) - (setq cmd (span-property span 'cmd)) - (cond - ;; comment: skip - ((eq (span-property span 'type) 'comment)) - ;; local qed: enter block - ((proof-string-match isar-save-command-regexp cmd) - (setq lev (+ lev 1))) - ;; local goal: leave block, or done - ((proof-string-match isar-local-goal-command-regexp cmd) - (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) - ;; global goal: done - ((proof-string-match isar-goal-command-regexp cmd) - (setq ans 'yes)))) + ;; FIXME da: bug was here -- there may be no previous span!! + (if span ; da: added, don't know if right + (progn ; da: added, don't know if right + (setq cmd (span-property span 'cmd)) + (cond + ;; comment: skip + ((eq (span-property span 'type) 'comment)) + ;; local qed: enter block + ((proof-string-match isar-save-command-regexp cmd) + (setq lev (+ lev 1))) + ;; local goal: leave block, or done + ((proof-string-match isar-local-goal-command-regexp cmd) + (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) + ;; global goal: done + ((proof-string-match isar-goal-command-regexp cmd) + (setq ans 'yes)))))) (eq ans 'yes)))) (defvar isar-current-goal 1 |