aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1998-11-03 14:38:00 +0000
committerDavid Aspinall1998-11-03 14:38:00 +0000
commitf48f380a4f5a8a1daecfe75961ed8b73eaefcae5 (patch)
tree02bdcdc6631e9632b05a3b2e83d89c561830ade2 /doc
parent5a271121d0bdd20f535b3038a9831fdcfde67b0e (diff)
Minor improvements
Diffstat (limited to 'doc')
-rw-r--r--doc/NewDoc.texi11
-rw-r--r--doc/notes.txt17
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