Re: [PG-devel] pg-set-span-helphighlights

[Paul A. Steckler]

I just ran the experiment of setting the properties used in the
helphighlight spans in the vanilla spans.

All works well, until you try to hide a span. Indeed, the span gets
hidden, using the 'invisible property. If you want to show it again,
you no longer get the context menu ... because the span is hidden.

Also, I've found there's some other functionality associated with the
helphighlights spans. In the old PG, there were special "goalsave"
spans, which I had thought existed because old versions of Coq did not
allow single-step undo. I've discovered that there are helphighlight
spans for proofs and sections, so you can hide them. I suppose I'll
have to work to restore this functionality. Of course, adding these
spans again will take additional run time.

-- Paul

On Fri, Feb 24, 2017 at 1:28 PM, Clément Pit--Claudel
 wrote:
> 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  
>> wrote:
>>> On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
>>>  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

Re: [PG-devel] pg-set-span-helphighlights

[Clément Pit--Claudel]

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  
> wrote:
>> On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
>>  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

Re: [PG-devel] pg-set-span-helphighlights

[Paul A. Steckler]

On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
 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

Re: [PG-devel] pg-set-span-helphighlights

[Clément Pit--Claudel]

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?

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
> 



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

Re: [PG-devel] pg-set-span-helphighlights

[Paul A. Steckler]

Yes, I tried having that procedure return nil, and ran the example
mentioned in this issue:

  https://github.com/psteckler/ProofGeneral/issues/82

On my laptop, the run time was reduced from 48 seconds to 44 seconds.

-- Paul



On Fri, Feb 24, 2017 at 3:36 AM, Pierre Courtieu
 wrote:
> Did you try to unplug it to see if the speed up is significant?
> I guess it is useful only when going back and forth in a script is slow.
> P
>
> Le ven. 24 févr. 2017 à 01:19, Clément Pit--Claudel 
> a écrit :
>>
>> On 2017-02-23 17:14, Paul A. Steckler wrote:
>> > 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.
>>
>> I use it from time to time; I think that's also what PG-movie is based on,
>> though I don't think anyone really uses that.
>>
>> > In PG/xml, that's not so useful, since the last response is an XML
>> > blob.
>>
>> True, but doesn't that XML usually contain what the old PG would have
>> called the "last response"? It would be either a message or a goal.
>>
>> Clément.
>>
>> ___
>> 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

Re: [PG-devel] pg-set-span-helphighlights

[Pierre Courtieu]

Did you try to unplug it to see if the speed up is significant?
I guess it is useful only when going back and forth in a script is slow.
P

Le ven. 24 févr. 2017 à 01:19, Clément Pit--Claudel 
a écrit :

> On 2017-02-23 17:14, Paul A. Steckler wrote:
> > 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.
>
> I use it from time to time; I think that's also what PG-movie is based on,
> though I don't think anyone really uses that.
>
> > In PG/xml, that's not so useful, since the last response is an XML
> > blob.
>
> True, but doesn't that XML usually contain what the old PG would have
> called the "last response"? It would be either a message or a goal.
>
> Clément.
>
> ___
> 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

Re: [PG-devel] pg-set-span-helphighlights

[Clément Pit--Claudel]

On 2017-02-23 17:14, Paul A. Steckler wrote:
> 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.

I use it from time to time; I think that's also what PG-movie is based on, 
though I don't think anyone really uses that.

> In PG/xml, that's not so useful, since the last response is an XML
> blob.

True, but doesn't that XML usually contain what the old PG would have called 
the "last response"? It would be either a message or a goal.

Clément.



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