diff options
| author | Makarius Wenzel | 1999-05-25 08:13:48 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-05-25 08:13:48 +0000 |
| commit | cab99ec2d9ea48a99ae1398023b3586e8849cf67 (patch) | |
| tree | ceb4d140c5701356a36bf9e2a917dc3a33423d85 | |
| parent | 5e8e51f9a6d9b5e56ec5e918bdf6fdb90180ab9b (diff) | |
proof-done-advancing: added proof-really-save-command-p to support
more general qed schemes, such as Isabelle/Isar's nested proofs;
| -rw-r--r-- | generic/proof-script.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 97f72be1..f9a7231d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -662,7 +662,8 @@ the ACS is marked in the current buffer. If CMD does not match any, ((eq (span-property span 'type) 'comment) (set-span-property span 'mouse-face 'highlight)) ((proof-check-atomic-sequents-lists span cmd end)) - ((proof-string-match proof-save-command-regexp cmd) + ((and (proof-string-match proof-save-command-regexp cmd) + (funcall proof-really-save-command-p span cmd)) ;; In coq, we have the invariant that if we've done a save and ;; there's a top-level declaration then it must be the ;; associated goal. (Notice that because it's a callback it |