diff options
| -rw-r--r-- | generic/proof-script.el | 7 |
1 files changed, 4 insertions, 3 deletions
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)) |