diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-02-05 21:58:53 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-02-05 21:58:53 +0000 |
| commit | 4087a0029d01da88c0c92f5a6a9fe1b1fb56d28a (patch) | |
| tree | d3551ced9243361cdda61fe1c3a3ba3f577690ae /isar/isar-unicode-tokens.el | |
| parent | 11a72e26c002afc307da2674181663d1b423b534 (diff) | |
Remove ligature/latin1 symbols. Trim short cuts
Diffstat (limited to 'isar/isar-unicode-tokens.el')
| -rw-r--r-- | isar/isar-unicode-tokens.el | 33 |
1 files changed, 7 insertions, 26 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index 5a885545..383034a5 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -453,30 +453,12 @@ ("thinspace" . " ") ("notni" . "∌") ("colonequals" . "≔") - ("foursuperior" . "⁴") ("fivesuperior" . "⁵") ("sixsuperior" . "⁶") ("sevensuperior" . "⁷") ("eightsuperior" . "⁸") - ("ninesuperior" . "⁹") - ;; ligatures, etc, unlikely to be useful? - ("oe" . "œ") - ("OE" . "Œ") - ("ae" . "æ") - ("AE" . "Æ") - ("aa" . "å") - ("AA" . "Å") - ("o" . "ø") ;; LaTeX \o - ("O" . "Ø") ;; LaTeX \O - ("l" . "ł") ;; LaTeX \l - ("L" . "Ł") ;; LaTeX \L - ("ss" . "ß") ;; LaTeX \ss - ("ff" . "ff") - ("fi" . "fi") - ("fl" . "fl") - ("ffi" . "ffi") - ("ffl" . "ffl")) + ("ninesuperior" . "⁹")) "Table mapping Isabelle ``xsymbol'' token names to Unicode strings. You can adjust this table to add more entries, or to change entries for @@ -541,20 +523,19 @@ results will be undefined when files are saved." ("==>" . "⟹") ("<==>" . "⟷") ("|-->" . "⟼") - ("<--" . "←⎯") ("<-->" . "⟷") ("<<" . "⟪") ("[|" . "⟦") (">>" . "⟫") ("|]" . "⟧") ("``" . "”") - ("''" . "“") - ("--" . "–") +; ("''" . "“") +; ("--" . "–") ("---" . "—") - ("''" . "″") - ("'''" . "‴") - ("''''" . "⁗") - (":=" . "≔") +; ("''" . "″") +; ("'''" . "‴") +; ("''''" . "⁗") +; (":=" . "≔") ;; some word shortcuts, started with backslash otherwise ;; too annoying. ("\nat" . "ℕ") |