From 897b459507e06883ae2169370271ad5a7a9749ea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 18 Jul 2002 17:43:37 +0000
Subject: More on keybindings: include old x-symbol-isabelle bindings but using
 super.

---
 doc/ProofGeneral.texi | 34 ++++++++++++++++++++++++++++------
 1 file changed, 28 insertions(+), 6 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 82f07baf..bb775c7f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -222,8 +222,8 @@ other documentation, system downloads, etc.
 
 Proof General 3.4 adds improvements and also compatibility fixes for
 new versions of Emacs, in particular, for GNU Emacs 21, which adds
-most of the pretty features that have only been available to XEmacs
-users until now (toolbar and X-Symbol support).
+the remaining pretty features that have only been available to XEmacs
+users until now (the toolbar and X-Symbol support).
 
 One major improvement has been to provide better support for
 synchronization with Coq proof scripts; now Coq Proof General should
@@ -2258,10 +2258,32 @@ affect one prover, use a keymap name like @code{isar-mode-map} and
 evaluate after the library @code{isar} has been loaded.
 
 To find the names of the functions you may want to bind, look in this
-manual, or query current bindings interactively with @kbd{C-h k}
-(which works for menu operations as well).  As a last resort you could
-also examine the lisp files which make up Proof General, such
-as @file{proof-menu.el}, but that's only for the brave.
+manual, or query current bindings interactively with @kbd{C-h k}.  This
+command (@code{describe-key}) works for menu operations as well; also
+use it to discover the current key-bindings which you're losing by
+declarations such as those above.  By default, @kbd{C-n} is
+@code{next-line} and @kbd{C-b} is @code{backward-char-command}; neither
+are needed if you have working cursor keys.
+
+If you're using XEmacs and your keyboard has a @i{super} modifier (on my
+PC keyboard it has a Windows symbol and is next to the control key), you
+can freely bind keys on that modifier globally (since none are by using
+lisp like this:
+@lisp
+(global-set-key [(super l)] 'x-symbol-INSERT-lambda)
+(global-set-key [(super n)] 'x-symbol-INSERT-notsign)
+(global-set-key [(super a)] 'x-symbol-INSERT-logicaland)
+(global-set-key [(super o)] 'x-symbol-INSERT-logicalor)
+(global-set-key [(super f)] 'x-symbol-INSERT-universal1)
+(global-set-key [(super t)] 'x-symbol-INSERT-existential1)
+(global-set-key [(super A)] 'x-symbol-INSERT-biglogicaland)
+(global-set-key [(super e)] 'x-symbol-INSERT-equivalence)
+(global-set-key [(super u)] 'x-symbol-INSERT-notequal)
+(global-set-key [(super m)] 'x-symbol-INSERT-arrowdblright)
+(global-set-key [(super i)] 'x-symbol-INSERT-longarrowright)
+@end lisp
+This defines a bunch of short-cuts for insert X-Symbol logical symbols
+which are often used in Isabelle.
 
 
 @node Using file variables
-- 
cgit v1.2.3