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
