Adds support for inserting more arrow characters by their LaTex names

original commit: a12491bb89030eda9635e0a1925dd60c8ea6d668
2010-12-07 11:05:10 -06:00 · 2010-12-07 11:05:10 -06:00 · 2468f25c33
commit 2468f25c33
parent fdf79692b3
1 changed files with 4 additions and 4 deletions
--- a/collects/mrlib/tex-table.rkt
+++ b/collects/mrlib/tex-table.rkt
@ -28,15 +28,15 @@
    ("leftrightarrow" "↔")
    ("nearrow" "↗")
    ("Updownarrow" "⇕")
-   
+    ("hookleftarrow" "↩")
+    ("hookrightarrow" "↪")
+    ("leadsto""↝")
+    
    ;; arrows that didn't come out right in copy & paste
    ;←− \longleftarrow
    ;⇐= \Longleftarrow 
-    ;← 􏰂 \hookleftarrow
    ;←→ \longleftrightarrow 
-    ;􏰁 → \hookrightarrow
    ;⇐⇒ \Longleftrightarrow
-    ;􏴲 \leadsto∗ 
    ;􏰃−→ \longmapsto
    ;=⇒ \Longrightarrow 
    ;􏰃→ \mapsto