Experimental use of fonts for \<AA> etc. Disable some contentious shortcuts

1 files changed, 134 insertions, 120 deletions

diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index e58ef9d3..1d7c3bf2 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -22,126 +22,140 @@
 (defconst isar-next-character-regexp "\\\\<#[xX][0-9A-Fa-f]+>\\|.")
 
 (defcustom isar-token-name-alist
-  '(; token name, unicode char sequence
+  (flet 
+      ((script (s) (format "\<^bscript>%s\<^escript>" s))
+       (frakt (s) (format "\<^bfrak>%s\<^efrak>" s))
+       (serif (s) (format "\<^bserif>%s\<^eserif>" s))
+       (bold (s) (format "\<^bbold>%s\<^ebold>" s)))
+
+    ;; property-based annotations.  More direct for input
+    ;; but inverse mapping tricky: need to ignore for 
+    ;; reverse and fold \<^bscript>A\<^escript> -> \<AA> etc.
+    ;; Extra dimension in table required.
+    ;; (Also: not supported in XEmacs?)
+      ;((script (s) (unicode-tokens-annotate-string "script" s))
+      ; (frakt    (s) (unicode-tokens-annotate-string "frak" s))
+      ; (serif     (s) (unicode-tokens-annotate-string "serif" s)))
+  `(; token name, unicode char sequence
     ;; Based on isabellesym.sty,v 1.45 2006/01/05
 
-    ;; Bold numerals: here subscripts 
-    ("one" . "₁")
-    ("two" . "₂")
-    ("three" . "₃")
-    ("four" . "₄")
-    ("five" . "₅")
-    ("six" . "₆")
-    ("seven" . "₇")
-    ("eight" . "₈")
-    ("nine" . "₉")
+    ;; Bold numerals
+    ("one" . ,(bold "1"))
+    ("two" . ,(bold "2"))
+    ("three" . ,(bold "3"))
+    ("four" . ,(bold "4"))
+    ("five" . ,(bold "5"))
+    ("six" . ,(bold "6"))
+    ("seven" . ,(bold "7"))
+    ("eight" . ,(bold "8"))
+    ("nine" . ,(bold "9"))
     ;; Mathcal 
-;;     ("A" . "")
-;;     ("B" . "")
-;;     ("C" . "")
-;;     ("D" . "")
-;;     ("E" . "")
-;;     ("F" . "")
-;;     ("G" . "")
-;;     ("H" . "")
-;;     ("I" . "")
-;;     ("J" . "")
-;;     ("K" . "")
-;;     ("L" . "")
-;;     ("M" . "")
-;;     ("N" . "")
-;;     ("O" . "")
-;;     ("P" . "")
-;;     ("Q" . "")
-;;     ("R" . "")
-;;     ("S" . "")
-;;     ("T" . "")
-;;     ("U" . "")
-;;     ("V" . "")
-;;     ("W" . "")
-;;     ("X" . "")
-;;     ("Y" . "")
-;;     ("Z" . "")
+    ("A" . ,(script "A"))
+    ("B" . ,(script "B"))
+    ("C" . ,(script "C"))
+    ("D" . ,(script "D"))
+    ("E" . ,(script "E"))
+    ("F" . ,(script "F"))
+    ("G" . ,(script "G"))
+    ("H" . ,(script "H"))
+    ("I" . ,(script "I"))
+    ("J" . ,(script "J"))
+    ("K" . ,(script "K"))
+    ("L" . ,(script "L"))
+    ("M" . ,(script "M"))
+    ("N" . ,(script "N"))
+    ("O" . ,(script "O"))
+    ("P" . ,(script "P"))
+    ("Q" . ,(script "Q"))
+    ("R" . ,(script "R"))
+    ("S" . ,(script "S"))
+    ("T" . ,(script "T"))
+    ("U" . ,(script "U"))
+    ("V" . ,(script "V"))
+    ("W" . ,(script "W"))
+    ("X" . ,(script "X"))
+    ("Y" . ,(script "Y"))
+    ("Z" . ,(script "Z"))
     ;; Math roman
-;;     ("a" . "")
-;;     ("b" . "")
-;;     ("c" . "")
-;;     ("d" . "")
-;;     ("e" . "")
-;;     ("f" . "")
-;;     ("g" . "")
-;;     ("h" . "")
-;;     ("i" . "")
-;;     ("j" . "")
-;;     ("k" . "")
-;;     ("l" . "")
-;;     ("m" . "")
-;;     ("n" . "")
-;;     ("o" . "")
-;;     ("p" . "")
-;;     ("q" . "")
-;;     ("r" . "")
-;;     ("s" . "")
-;;     ("t" . "")
-;;     ("u" . "")
-;;     ("v" . "")
-;;     ("w" . "")
-;;     ("x" . "")
-;;     ("y" . "")
-;;     ("z" . "")
+    ("a" . ,(serif "a"))
+    ("b" . ,(serif "b"))
+    ("c" . ,(serif "c"))
+    ("d" . ,(serif "d"))
+    ("e" . ,(serif "e"))
+    ("f" . ,(serif "f"))
+    ("g" . ,(serif "g"))
+    ("h" . ,(serif "h"))
+    ("i" . ,(serif "i"))
+    ("j" . ,(serif "j"))
+    ("k" . ,(serif "k"))
+    ("l" . ,(serif "l"))
+    ("m" . ,(serif "m"))
+    ("n" . ,(serif "n"))
+    ("o" . ,(serif "o"))
+    ("p" . ,(serif "p"))
+    ("q" . ,(serif "q"))
+    ("r" . ,(serif "r"))
+    ("s" . ,(serif "s"))
+    ("t" . ,(serif "t"))
+    ("u" . ,(serif "u"))
+    ("v" . ,(serif "v"))
+    ("w" . ,(serif "w"))
+    ("x" . ,(serif "x"))
+    ("y" . ,(serif "y"))
+    ("z" . ,(serif "z"))
     ;; Fraktur
-;;     ("AA" . "")
-;;     ("BB" . "")
-;;     ("CC" . "")
-;;     ("DD" . "")
-;;     ("EE" . "")
-;;     ("FF" . "")
-;;     ("GG" . "")
-;;     ("HH" . "")
-;;     ("II" . "")
-;;     ("JJ" . "")
-;;     ("KK" . "")
-;;     ("LL" . "")
-;;     ("MM" . "")
-;;     ("NN" . "")
-;;     ("OO" . "")
-;;     ("PP" . "")
-;;     ("QQ" . "")
-;;     ("RR" . "")
-;;     ("SS" . "")
-;;     ("TT" . "")
-;;     ("UU" . "")
-;;     ("VV" . "")
-;;     ("WW" . "")
-;;     ("XX" . "")
-;;     ("YY" . "")
-;;     ("ZZ" . "")
-;;     ("aa" . "")
-;;     ("bb" . "")
-;;     ("cc" . "")
-;;     ("dd" . "")
-;;     ("ee" . "")
-;;     ("ff" . "")
-;;     ("gg" . "")
-;;     ("hh" . "")
-;;     ("ii" . "")
-;;     ("jj" . "")
-;;     ("kk" . "")
-;;     ("ll" . "")
-;;     ("mm" . "")
-;;     ("nn" . "")
-;;     ("oo" . "")
-;;     ("pp" . "")
-;;     ("qq" . "")
-;;     ("rr" . "")
-;;     ("ss" . "")
-;;     ("tt" . "")
-;;     ("uu" . "")
-;;     ("vv" . "")
-;;     ("ww" . "")
-;;     ("xx" . "")
-;;     ("yy" . "")
-;;     ("zz" . "")
+    ("AA" . ,(frakt "A"))
+    ("BB" . ,(frakt "B"))
+    ("CC" . ,(frakt "C"))
+    ("DD" . ,(frakt "D"))
+    ("EE" . ,(frakt "E"))
+    ("FF" . ,(frakt "F"))
+    ("GG" . ,(frakt "G"))
+    ("HH" . ,(frakt "H"))
+    ("II" . ,(frakt "I"))
+    ("JJ" . ,(frakt "J"))
+    ("KK" . ,(frakt "K"))
+    ("LL" . ,(frakt "L"))
+    ("MM" . ,(frakt "M"))
+    ("NN" . ,(frakt "N"))
+    ("OO" . ,(frakt "O"))
+    ("PP" . ,(frakt "P"))
+    ("QQ" . ,(frakt "Q"))
+    ("RR" . ,(frakt "R"))
+    ("SS" . ,(frakt "S"))
+    ("TT" . ,(frakt "T"))
+    ("UU" . ,(frakt "U"))
+    ("VV" . ,(frakt "V"))
+    ("WW" . ,(frakt "W"))
+    ("XX" . ,(frakt "X"))
+    ("YY" . ,(frakt "Y"))
+    ("ZZ" . ,(frakt "Z"))
+    ("aa" . ,(frakt "a"))
+    ("bb" . ,(frakt "b"))
+    ("cc" . ,(frakt "c"))
+    ("dd" . ,(frakt "d"))
+    ("ee" . ,(frakt "e"))
+    ("ff" . ,(frakt "f"))
+    ("gg" . ,(frakt "g"))
+    ("hh" . ,(frakt "h"))
+    ("ii" . ,(frakt "i"))
+    ("jj" . ,(frakt "j"))
+    ("kk" . ,(frakt "k"))
+    ("ll" . ,(frakt "l"))
+    ("mm" . ,(frakt "m"))
+    ("nn" . ,(frakt "n"))
+    ("oo" . ,(frakt "o"))
+    ("pp" . ,(frakt "p"))
+    ("qq" . ,(frakt "q"))
+    ("rr" . ,(frakt "r"))
+    ("ss" . ,(frakt "s"))
+    ("tt" . ,(frakt "t"))
+    ("uu" . ,(frakt "u"))
+    ("vv" . ,(frakt "v"))
+    ("ww" . ,(frakt "w"))
+    ("xx" . ,(frakt "x"))
+    ("yy" . ,(frakt "y"))
+    ("zz" . ,(frakt "z"))
     ("alpha" . "α")
     ("beta" . "β")
     ("gamma" . "γ")
@@ -458,8 +472,8 @@
     ("sixsuperior" . "⁶")
     ("sevensuperior" . "⁷")
     ("eightsuperior" . "⁸")
-    ("ninesuperior" . "⁹"))
-  "Table mapping Isabelle ``symbol'' token names to Unicode strings.
+    ("ninesuperior" . "⁹")))
+  "Table mapping Isabelle symbol token names to Unicode strings.
 
 You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
@@ -477,8 +491,8 @@ results will be undefined when files are saved."
 
 (defcustom isar-shortcut-alist
   '(; short cut, unicode string
-    ("<>" . "⋄")
-    ("|>" . "⊳")
+;    ("<>" . "⋄")
+;    ("|>" . "⊳")
     ("\\/" . "∨")
     ("/\\" . "∧")
     ("+O" . "⊕")
@@ -516,7 +530,7 @@ results will be undefined when files are saved."
     ("=>" . "⇒")
     ("<->" . "↔")
     ("<=>" . "⇔")
-    ("|->" . "↦")
+;    ("|->" . "↦") 
     ("<--" . "⟵")
     ("<==" . "⟸")
     ("-->" . "⟶")