diff options
Diffstat (limited to 'ghilbert.py')
| -rwxr-xr-x | ghilbert.py | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/ghilbert.py b/ghilbert.py index 19e7bef..cb4f106 100755 --- a/ghilbert.py +++ b/ghilbert.py @@ -1354,7 +1354,7 @@ class Ghilbert(): pip.proof.append(e) - def add_thm(self, expr): + def add_thm(self, expr, stop_cond): """Initial processing for a thm statement expr is the thm's s-expression @@ -1445,7 +1445,10 @@ class Ghilbert(): pip.dvs = self.dv_canonical(expr, pip_vdict) try: - for j in xrange(len(expr[4])): + nsteps = len(expr[4]) + for j in xrange(nsteps): + if j == stop_cond: + raise GhError(_("Step.")) step = expr[4][j] self.thm_step(pip, step) except GhError, x: @@ -2150,7 +2153,7 @@ class Ghilbert(): self.interfaces[ifname] = child self.push_history((Ghilbert.EXPORT, child, path)) - def read_proof_file_from_scanner(self, scanner, one_only): + def read_proof_file_from_scanner(self, scanner, stop_cond): while (1): self.pip = None @@ -2164,7 +2167,7 @@ class Ghilbert(): raise VerifyError( _("Expected s-expression (...) command argument")) if word == 'thm': - self.add_thm(sexpr) + self.add_thm(sexpr, stop_cond) elif word == 'def': self.add_def(sexpr) elif word == 'var': @@ -2183,7 +2186,7 @@ class Ghilbert(): self.log.warning(_("Skipping unknown command '%s'") % word) scanner.set_good() - if one_only: + if stop_cond >= -1: break |