Opened 14 years ago
Closed 14 years ago
#347 closed enhancement (fixed)
Slight change in proof-store-buffer-win to enable undo in the Notepad
| Reported by: | Erik Martin-Dorel | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.0 |
| Component: | 7:prover-coq | Keywords: | |
| Cc: | Erik Martin-Dorel |
Description
The functions proof-store-goals-win and proof-store-response-win
are really convenient, but I would like to propose an improvement.
Currently, the buffer name " response-freeze" begins with a space, which disable undo. Consequently, if ever the user makes an unwanted edit such as a deletion, he will not be able to recover it.
Thus enabling undo would make these functions even more user-friendly.
Moreover, this undo feature is quite standard, since it is enabled in
the buffer *Shell Command Output* handled by the GNU Emacs function
shell-command.
To conclude, I would suggest to replace " response-freeze" with
"*response-freeze*" in proof-store-buffer-win.
Kind regards, Erik Martin-Dorel.
Note: See
TracTickets for help on using
tickets.
Done. Thanks for proposal.