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

Reply via email to