From 79f2bcbae8e82f9f20defa84e23427204a376b82 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 9 Aug 2002 11:11:16 +0000
Subject: Fix proof-disappearing-proofs; comments

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

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 666495ff..de4e36e8 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -615,7 +615,7 @@ NAME does not need to be unique."
 		       (cons span (span-property controlspan 'children)))
     (pg-set-span-helphighlights span 'nohighlight)
     (if proof-disappearing-proofs 
-	(pg-make-element-invisible "proof" name))))
+	(pg-make-element-invisible "proof" proofid))))
 
 (defun pg-span-name (span)
   "Return a user-level name for SPAN."
@@ -1479,7 +1479,8 @@ With ARG, turn on scripting iff ARG is positive."
 		    proof-unnamed-theorem-name))
 
       ;; NB: if extending an already closed region, ought to delete
-      ;; the body and extend that too: this makes multiple nested bodies.[?]
+      ;; the body and extend that too: currently we make multiple nested 
+      ;; bodies, a bit messy.
       ;; (NB: savestart used for nested region: here use saveend)
       (proof-make-goalsave gspan
 			   (+ (span-start gspan) 
-- 
cgit v1.2.3