diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-05-03 13:06:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-05-03 13:06:56 +0000 |
| commit | 1f01dac278d97b9c40f5f178f1b5fac4df8239ec (patch) | |
| tree | 2908c08b1bbdd6bd6b812d7ef1eaaea63df41f38 /isar | |
| parent | d27fd2076ef8ad5801c784f7727efcf8a1380637 (diff) | |
Add support for proof-next-error.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el index e26a7f91..bc4729a9 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -155,6 +155,7 @@ proof-state-preserving-p 'isar-state-preserving-p proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list)) + (defun isar-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle/Isar." (setq @@ -372,8 +373,12 @@ proof-shell-retract-files-regexp." (setq str (span-property span 'cmd)) (setq ans nil) (cond - ;; comment or diagnostic command: skip + ;; 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) ((or (eq (span-property span 'type) 'comment) + (eq (span-property span 'type) 'proof); da: needed? (proof-string-match isar-undo-skip-regexp str) (proof-string-match isar-undo-ignore-regexp str))) ;; finished goal: undo |