diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2002-02-12 18:25:13 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2002-02-12 18:25:13 +0000 |
| commit | 72bd3a0e259003fae2469042d4fdd579f75953cf (patch) | |
| tree | 606e1f60f261517fda5d1080951574471b74e952 /isar | |
| parent | e50d2fc11b2ec1c6e6d3bed4bdbf99aea092cbff (diff) | |
observe isar-undo-ignore-regexp in isar-count-undos and isar-find-and-forget;
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/isar/isar.el b/isar/isar.el index 4160e809..e26a7f91 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -348,8 +348,9 @@ proof-shell-retract-files-regexp." (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'vanilla) (or (proof-string-match isar-undo-skip-regexp str) + (proof-string-match isar-undo-ignore-regexp str) (setq ct (+ 1 ct)))) - ((eq (span-property span 'type) 'pbp) + ((eq (span-property span 'type) 'pbp) ;FIXME dead code? ;; this case probably redundant for Isabelle, unless ;; we think of some nice ways of matching non-undoable ;; commands. @@ -373,7 +374,8 @@ proof-shell-retract-files-regexp." (cond ;; comment or diagnostic command: skip ((or (eq (span-property span 'type) 'comment) - (proof-string-match isar-undo-skip-regexp str))) + (proof-string-match isar-undo-skip-regexp str) + (proof-string-match isar-undo-ignore-regexp str))) ;; finished goal: undo ((eq (span-property span 'type) 'goalsave) (setq ans isar-undo)) |