A wild guess: the extra runtime is due to adding extra overlays.  This was 
needed in the original PG since there may not have been another overlay 
covering exactly that region (because the locked region was one large overlay). 
 But since there now is one overlay per small processed region, that overlay 
can be reused in pg-set-span-helphighlights.

Is that correct?

On 2017-02-23 17:14, Paul A. Steckler wrote:
> In my PG/xml fork, the Elisp profiler indicates the most expensive
> procedure is `proof-done-advancing-other' (about 12% of the CPU
> cycles). Most of the time in that procedure is allotted to
> `pg-set-span-helphighlights'.
> 
> That procedure creates a daughter span with a context menu. In vanilla
> PG, it looks like the context menu also contains the last response
> from Coq. In PG/xml, that's not so useful, since the last response is
> an XML blob.
> 
> The context menu has a Show/Hide menu item. I suppose that can be
> useful. There's also a Copy menu item, but of course you can use
> ordinary Emacs commands for that.
> 
> Do we know if this functionality is widely-used? How grievous would it
> be if I removed it?
> 
> -- Paul
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to