From 7bba8979740b428d6cfad43b2906bf3dcafd2454 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 11 Jun 2002 21:00:23 +0000
Subject: Only match saves for prover that supports nested proofs (restores old
 behaviour for Isar).  Isar goal/save regexps dont match up properly.

---
 generic/proof-script.el | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4996bcd1..3bd03042 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1264,9 +1264,10 @@ the ACS is marked in the current buffer. If CMD does not match any,
 		 ;; Ignore comments, any nested goalsaves
 		 ((eq (span-property gspan 'type) 'comment))
 		 ((eq (span-property gspan 'type) 'goalsave))
-		 ;; Increment depth for a nested save
-		 ((and proof-save-command-regexp
-		       ;; NB: not doing really save command here
+		 ;; Increment depth for a nested save, in case
+		 ;; prover supports history of nested proofs
+		 ((and proof-nested-goals-p
+		       proof-save-command-regexp
 		       (proof-string-match proof-save-command-regexp cmd))
 		  (incf lev))
 		 ;; Decrement depth when a goal is hit
-- 
cgit v1.2.3