From 39419dc46d4cf8e055ff7e8a29028dec44e9acf7 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 9 Sep 2009 23:19:07 +0000
Subject: Delete the pghelp spans for now, after all.

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

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index aa54c5fa..d3f64ab3 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -296,9 +296,10 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
 (defun proof-script-delete-spans (beg end)
   "Delete spans between BEG and END."
   (span-delete-spans beg end 'type)
-  (span-delete-spans beg end 'idiom))
-;; TODO: we should delete these ones when they're edited
-;;   (span-delete-spans beg end 'pghelp))
+  (span-delete-spans beg end 'idiom)
+  ;; TODO: we might keep these spans around, but delete them ones when
+  ;; they're edited.  Needs more thought to avoid utter confusion.
+  (span-delete-spans beg end 'pghelp))
 
 
 
-- 
cgit v1.2.3