From 4087a0029d01da88c0c92f5a6a9fe1b1fb56d28a Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 5 Feb 2008 21:58:53 +0000
Subject: Remove ligature/latin1 symbols. Trim short cuts

---
 isar/isar-unicode-tokens.el | 33 +++++++--------------------------
 1 file changed, 7 insertions(+), 26 deletions(-)

(limited to 'isar/isar-unicode-tokens.el')

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" . "ℕ")
-- 
cgit v1.2.3