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.
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.
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list