diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-11 21:00:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-11 21:00:23 +0000 |
| commit | 7bba8979740b428d6cfad43b2906bf3dcafd2454 (patch) | |
| tree | 38c937474b67c44d93e0633e59436eceeefeaf83 /generic | |
| parent | 18111fbde76762f2e6e02005741754b0967fdb4b (diff) | |
Only match saves for prover that supports nested proofs (restores old behaviour for Isar). Isar goal/save regexps dont match up properly.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 7 |
1 files changed, 4 insertions, 3 deletions
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 |