Great news :) On 2017-02-24 12:02, Paul A. Steckler wrote: > 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 >
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
