I think there is no problem with that.

Le ven. 24 févr. 2017 à 22:49, Paul A. Steckler <st...@stecksoft.com> 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 completed, there's another help span that covers the
> entire proof. If you choose Hide from its context menu, the entire
> proof is hidden. Before the proof is completed, you can hide an
> individual tactic call -- not sure why you'd do that -- but you don't
> seem to able to show it again (a bug, apparently). The only other
> items on the context menu for an individual script item are Undo and
> Copy, which you can already do in other ways. For help spans
> associated with proofs, there are Print and Check menu items.
>
> Would it make sense to omit the help spans on individual items, and
> just have the help spans for proofs and sections? That would give
> decent speedup, at only a small cost (so I claim) of functionality.
>
> -- Paul
>
>
>
>
> On Fri, Feb 24, 2017 at 2:36 PM, Paul A. Steckler <st...@stecksoft.com>
> wrote:
> > 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
> > <clement....@gmail.com> 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 <
> 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
> >>>
> >>
> _______________________________________________
> 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

Reply via email to