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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to