diff options
| author | David Aspinall | 2009-09-09 23:19:07 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-09 23:19:07 +0000 |
| commit | 39419dc46d4cf8e055ff7e8a29028dec44e9acf7 (patch) | |
| tree | 32515d9adedfbfb2679099bb7ce37ba82669b22a /generic/proof-script.el | |
| parent | 1583eb204e175319583b639d2786913f78b8e490 (diff) | |
Delete the pghelp spans for now, after all.
Diffstat (limited to 'generic/proof-script.el')
| -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)) |