Skip to content

Commit

Permalink
Remove pghelp spans when retracting.
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Matafou committed Jun 18, 2019
1 parent cdc630c commit 2ada467
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions generic/proof-script.el
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)."
Expand Down

0 comments on commit 2ada467

Please sign in to comment.