diff options
| author | David Aspinall | 2002-06-12 10:33:18 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-06-12 10:33:18 +0000 |
| commit | ce2ceb08d8de338876e34730c061c9d02548c4be (patch) | |
| tree | f5fe3bde41ba71f5d4d98a89b3337d985db347c0 /generic/proof-script.el | |
| parent | 54bf12bbf49e62d3afb92b67b1ec4f7a4f682666 (diff) | |
Adjust proof-nesting depth, add FIXME notes since not right yet
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 30692c92..78c9d3d3 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2055,6 +2055,12 @@ appropriate." ;; straightforward ;; +;; FIXME: we need to adjust proof-nesting-depth appropriately here. +;; It would help to know the type of retraction which has just +;; occurred: a kill-proof may be assumed to set nesting depth +;; to zero; an undo sequence may alter it some other way. +;; FIXME FIXME: at the moment, the adjustment is made in +;; the wrong place!! (defun proof-done-retracting (span) "Callback for proof-retract-until-point. We update display after proof process has reset its state. @@ -2147,6 +2153,10 @@ up to the end of the locked region." ;; Otherwise, start the retraction by killing off the ;; currently active goal. ;; FIXME: and couldn't we move the end upwards? + ;; FIXME: hack proof-nesting-depth here. This is + ;; in the wrong place: it should be done *after* the + ;; retraction has succeeded. + (setq proof-nesting-depth (1- proof-nesting-depth)) (setq actions (proof-setup-retract-action (span-start span) end proof-kill-goal-command |