And I can confirm it's the span-making that takes the time. If I set the properties on the existing vanilla span, the time is about the same as just returning nil.
On Fri, Feb 24, 2017 at 11:46 AM, Paul A. Steckler <st...@stecksoft.com> wrote: > 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
