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
> 

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