diff options
| author | Pierre Courtieu | 2019-06-18 15:28:24 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2019-06-18 15:28:24 +0200 |
| commit | 2ada467c2c2964a605659714f2a267db2c915952 (patch) | |
| tree | 7d3fbf40a738f04e482a4117083431f37252aa41 /generic | |
| parent | cdc630c3d453fe0c1384e3faca268f9818828c26 (diff) | |
Remove pghelp spans when retracting.
Due to performance issue (probably an emacs bug) and given the
uselessness of the pghelp spans in retracted regions. We simply remove
these spans when retracting.
The question remains to remove them completely or to make them more
useful. company-coq currently disables them anyway.
Diffstat (limited to 'generic')
| -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)." |