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
