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 :)


Attachment: 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

Reply via email to