Well, the current goal should always be shown, unless there's a bug.
Of course, that was probably the intended behavior of the old version.

An alternative to removing the button would be to relocate it to the
right of its current position, so that it appears in the pull-down
menu with other, less-used buttons. After the new PG has had some use,
we could assess whether the State button can be scrapped.

-- Paul


On Mon, Aug 8, 2016 at 12:14 PM, Clément Pit--Claudel
<clement....@gmail.com> wrote:
> 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 :)
>
>
>
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to