From cab99ec2d9ea48a99ae1398023b3586e8849cf67 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 25 May 1999 08:13:48 +0000
Subject: proof-done-advancing: added proof-really-save-command-p to support
 more general qed schemes, such as Isabelle/Isar's nested proofs;

---
 generic/proof-script.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

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
-- 
cgit v1.2.3