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