I've made some fair headway in getting Proof General working with the coqtop XMLish protocol. So now I'm working on some of the less-central bits for that port.
There's a PG button, State, which in the REPL version of PG, sends "Show." to coqtop to request the current goal. I'm thinking this button can be removed, because the XML version of PG sends a goal request after each block of script is sent, and after undoing a line or lines, so that the current goal is always displayed. Also, I've added a button that works like CoqIDE's gears button, which checks the validity of the document. That means that toolbar real estate is at a premium, so anything I can remove is welcome. Is this button redundant, then? -- Paul _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
