On 2016-08-08 11:31, Paul A. Steckler wrote: > 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.
Hmm. In the old state there was a bunch of cases in which this got out of sync, and C-c C-p (which IIRC does the same as that button) was a nice way to fix it. But if this never happens anymore, then we can remove it :)
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
