diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 2 | ||||
| -rw-r--r-- | todo | 15 |
3 files changed, 18 insertions, 2 deletions
@@ -14,6 +14,9 @@ Generic Changes Buttons are automatically enabled or disabled as appropriate. This requires XEmacs 20.4 or better for reliable working. +* Menus and keybindings have been reorganized. + Now keybindings invoke same functions as toolbar. + * Terminal string now automatically added to command for C-c C-v * Cleaned up example files so all demonstrate same theorem "conj_comms". diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 504c19a3..3957c245 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -973,6 +973,8 @@ prover is processing it.} @code{proof-retract-until-point-interactive} @item C-c b @code{proof-process-buffer} +@item C-c r +@code{proof-retract-buffer} @item C-c @var{terminator-character} @code{proof-active-terminator-minor-mode} @end table @@ -42,8 +42,19 @@ A Pending work, in progress [da]: (fixup eye shadows, mag glass, finger, stop icon) - command and button for searching for a theorem (possibly matching a given constant, or the proof state). - - toolbar refresh problems - - investigation of excessive processing for large proofs + - reorganization and improvement of menus, keybindings + . use toolbar functions, but remove from proof-toolbar and reorganize. + . update documentation + - test support for x-symbol + - investigate toolbar refresh problems + - investigate of excessive processing for large proofs + - investigate bug fix for vacuous locked regions + +A Usability enhancement: + Enable toolbar in other buffers. Should switch to active + scripting buffer first if it is non current. + (In fact, a sensible subset of scripting commands would + work from other buffers). A Usability enhancement: Movement of point after assert/retract commands |