From ecd74a6acd3ba9a200d36c7d915d56e7b2c3be9b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 17 Feb 2008 12:30:02 +0000 Subject: Experimental use of fonts for \ etc. Disable some contentious shortcuts --- isar/isar-unicode-tokens.el | 254 +++++++++++++++++++++++--------------------- 1 file changed, 134 insertions(+), 120 deletions(-) (limited to 'isar/isar-unicode-tokens.el') 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> -> \ 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." ("=>" . "⇒") ("<->" . "↔") ("<=>" . "⇔") - ("|->" . "↦") +; ("|->" . "↦") ("<--" . "⟵") ("<==" . "⟸") ("-->" . "⟶") -- cgit v1.2.3