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
