OK, I've left the State button in, and it's working with the XML
protocol. I moved it over a few positions, so that the new Check
button is always visible.

Thanks for all the feedback.

-- Paul

On Tue, Aug 9, 2016 at 3:58 AM, Hendrik Tews <hendrik.t...@fireeye.com> wrote:
> Hi,
> "Paul A. Steckler" <st...@stecksoft.com> writes:
>> Well, the current goal should always be shown, unless there's a bug.
> What if the user deletes the emacs window containing the current
> goal because he temporarily wants to use that screen space for
> something else? I used to do this quite often when I needed to
> look into other files in the middle of the proof. When going back
> to the proof I would then hit C-c C-p.
> It should of course be fine if PG just redisplays a cached
> version of the current goal without talking to Coq when the user
> hits C-c C-p. The redisplay-goal functionality, however, should
> IMO be kept together with a button or menu entry. Of course, if
> you want to put more important stuff in the toolbar, a menu entry
> and a key binding are sufficient.
> Bye,
> Hendrik
> This email and any attachments thereto may contain private, confidential, 
> and/or privileged material for the sole use of the intended recipient. Any 
> review, copying, or distribution of this email (or any attachments thereto) 
> by others is strictly prohibited. If you are not the intended recipient, 
> please contact the sender immediately and permanently delete the original and 
> any copies of this email and any attachments thereto.
ProofGeneral-devel mailing list

Reply via email to