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
<pierre.court...@cnam.fr> 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 <clement....@gmail.com>
> 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

Reply via email to