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

Reply via email to