On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel <clement....@gmail.com> wrote: > 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?
I think you're right that it's the span creation is what adds the most time. In the original PG, there was already a span for each script item with the "type" property set to "vanilla". Those spans have links to the helphighlight spans. The helphighlight spans basically cover the same piece of text as the vanilla spans, except for any whitespace on the ends. In PG/xml, I'm already trimming any whitespace at the start of the vanilla spans, because those are the spans that get colors, otherwise the coloring looks bad. It may be possible to reuse the vanilla spans to contain the properties that were being set in the helphighlight spans. There is one call that also sets a face for these spans, which may clobber a face that's already been set. Making this change may simplify the code in other ways. Currently, there are separate calls to delete the vanilla spans and to delete the helphighlight spans. In one instance, there's a call to delete the vanilla spans, but not the helphighlight spans (in `proof-script-clear-queue-spans-on-error'); I don't understand why you'd delete just the vanilla spans. The helphighlight spans have modification hooks that delete them. If we reused the vanilla spans, we could add a modification hook that just removes the added properties. -- Paul > > 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 >> > > > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
