From 125fadc2db026434af39c0694f8de198d4ed57fc Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 4 Dec 2001 16:16:00 +0000
Subject: isar specific commands for bold/sup/sub;

---
 doc/ProofGeneral.texi | 20 +++++++++++++++++++-
 isar/isar.el          | 10 ++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0b5277ac..3575f480 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2827,7 +2827,7 @@ next start Proof General.
 * The default value for XEmacs built for solaris is nil, because
 of unreliabilities with enablers there.
 
-The default value is @code{t}.
+The default value is @code{nil}.
 @end defopt
 
 @c This one removed: proof-auto-retract
@@ -3710,6 +3710,24 @@ Shows all available commands of Isabelle/Isar's outer syntax.
 Shows theorems stored in the current theory node.
 @end table
 
+@kindex C-c C-a b
+@kindex C-c C-a u
+@kindex C-c C-a l
+
+The following shortcuts insert control sequences into the text,
+modifying the appearance of individual symbols (single letters,
+mathematical entities etc.); the X-Symbol package will provide immediate
+visual feedback.
+
+@table @kbd
+@item C-c C-a b
+Inserts "\<^bold>"
+@item C-c C-a u
+Inserts "\<^sup>"
+@item C-c C-a l
+Inserts "\<^sub>"
+@end table
+
 Command termination via `@code{;}' is an optional feature of Isar
 syntax.  Neither Isabelle/Isar nor Proof General require semicolons to
 do their job.  The following command allows to get rid of command
diff --git a/isar/isar.el b/isar/isar.el
index 56f7091c..db70761d 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -435,6 +435,16 @@ proof-shell-retract-files-regexp."
   (proof-string-match isar-undo-skip-regexp cmd))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Commands specific to isar                                      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(proof-defshortcut isar-bold "\\<^bold>" [(control b)])
+(proof-defshortcut isar-super "\\<^sup>" [(control u)])
+(proof-defshortcut isar-sub "\\<^sub>"   [(control l)])
+
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Isar shell startup and exit hooks                              ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3