diff options
| author | David Aspinall | 1998-11-03 14:38:00 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-03 14:38:00 +0000 |
| commit | f48f380a4f5a8a1daecfe75961ed8b73eaefcae5 (patch) | |
| tree | 02bdcdc6631e9632b05a3b2e83d89c561830ade2 | |
| parent | 5a271121d0bdd20f535b3038a9831fdcfde67b0e (diff) | |
Minor improvements
| -rw-r--r-- | doc/NewDoc.texi | 11 | ||||
| -rw-r--r-- | doc/notes.txt | 17 |
2 files changed, 17 insertions, 11 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index f565f2d3..e900efd9 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -202,8 +202,7 @@ keyboard. Type @kbd{C-h m} to get a list of keys for the current mode. The proof assistant is automatically started inside Emacs when you ask for some of the proof script to be processed. To follow an example use -of Proof General on a LEGO proof, see @pxref{Walkthrough example in -LEGO}. +of Proof General on a LEGO proof, see @pxref{Walkthrough example in LEGO}. If Proof General has not already been installed, you should insert the line: @@ -359,9 +358,9 @@ file, while it is written and edited. @unnumberedsubsec Goals and saves A proof script contains a sequence of commands used to prove one or more -theorems. In general we assume that for each proved theorem, -a proof script contains a goal .. save pair of commands which -look something like this: +theorems. In general we assume that for each proved theorem, a proof +script contains a goal .. save pair of commands which appear something +like this: @lisp goal T is G ... @@ -371,7 +370,7 @@ Proof General recognizes goal .. save pairs in proof scripts. The name T can appear in the definitions menu for the proof script (see Script definitions menu), and once a goal .. save pair is completed it is treated -as atomic when undoing proof steps (see Undo). +as atomic when undoing proof steps (see Undo). @node The buffer model, Regions in a proof script, Proof scripts, Basic Script Management diff --git a/doc/notes.txt b/doc/notes.txt index b8ca8fee..9b91c191 100644 --- a/doc/notes.txt +++ b/doc/notes.txt @@ -99,7 +99,7 @@ Get Dave a laptop to demo on. ********* -Support for fume-function. +Support for Function Menus fume-func is a handy package which makes a menu from the function declarations in a buffer. Proof General configures fume-func so @@ -108,10 +108,17 @@ that you can quickly jump to particular proofs in a script buffer. If you want to use fume-func, you may need to enable it for yourself. It is distributed with XEmacs (and FSF GNU Emacs) but by not enabled by default. To enable it you should find -the file fume-func.el and follow the instructions there. -If you have XEmacs 20.4, what you need to do is this: - - ...... +the file func-menu.el and follow the instructions there. +At the time of writing, the current version of XEmacs is 20.4 and +it has these instructions: + +(require 'func-menu) +(define-key global-map 'f8 'function-menu) +(add-hook 'find-file-hooks 'fume-add-menubar-entry) +(define-key global-map "\C-cl" 'fume-list-functions) +(define-key global-map "\C-cg" 'fume-prompt-function-goto) +(define-key global-map '(shift button3) 'mouse-function-menu) +(define-key global-map '(meta button1) 'fume-mouse-function-goto) If you have any other version of Emacs, you should check the fume-func.el file |
