From 72bd3a0e259003fae2469042d4fdd579f75953cf Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Tue, 12 Feb 2002 18:25:13 +0000 Subject: observe isar-undo-ignore-regexp in isar-count-undos and isar-find-and-forget; --- isar/isar.el | 6 ++++-- 1 file 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)) -- cgit v1.2.3