I think there is no problem with that.
Le ven. 24 févr. 2017 à 22:49, Paul A. Steckler a
écrit :
> Actually, it's not clear to me what's the utility for the help spans
> on individual script items.
>
> What happens in old PG is that each script item gets a help span, but
> once a proof is comple
Actually, it's not clear to me what's the utility for the help spans
on individual script items.
What happens in old PG is that each script item gets a help span, but
once a proof is completed, there's another help span that covers the
entire proof. If you choose Hide from its context menu, the en
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
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:
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 wi
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)
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
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 tr
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
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 an
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
11 matches
Mail list logo
