From 2ada467c2c2964a605659714f2a267db2c915952 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 18 Jun 2019 15:28:24 +0200 Subject: [PATCH] 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. --- generic/proof-script.el | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/generic/proof-script.el b/generic/proof-script.el index 4f2c4a713..761a3bbe9 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)."