From ce2ceb08d8de338876e34730c061c9d02548c4be Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 12 Jun 2002 10:33:18 +0000
Subject: Adjust proof-nesting depth, add FIXME notes since not right yet

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

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

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