diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 4f2c4a71..761a3bbe 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -353,7 +353,6 @@ deactivated." (if proof-active-buffer-fake-minor-mode (setq proof-active-buffer-fake-minor-mode nil)) (proof-script-delete-spans (point-min) (point-max)) - (proof-script-delete-secondary-spans (point-min) (point-max)) (setq pg-script-portions nil) (proof-detach-queue) (proof-detach-locked) @@ -405,7 +404,9 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (defun proof-script-delete-spans (beg end) "Delete primary spans between BEG and END. Secondary 'pghelp spans are left." (span-delete-spans beg end 'type) - (span-delete-spans beg end 'idiom)) + (span-delete-spans beg end 'idiom) + (span-delete-spans beg end 'pg-span) + ) (defun proof-script-delete-secondary-spans (beg end) "Delete secondary spans between BEG and END (currently, 'pghelp spans)." |