"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.


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