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
> 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
>>> 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 mailing list
ProofGeneral-devel mailing list