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
