diff options
| author | Nickolai Zeldovich | 2020-03-03 23:20:43 -0500 |
|---|---|---|
| committer | Nickolai Zeldovich | 2020-03-03 23:20:43 -0500 |
| commit | 235260cfa775005ab6a94697e96e2822a72be03d (patch) | |
| tree | ceaaad7d243687567eefa95c21a7150b6b9b198e | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
Remove invisible U+FE00 variation selector from CoqIDE bindings
The current CoqIDE bindings include an invisible U+FE00 variation selector
immediately following a number of symbols. For example, \empty maps to
U+2205 U+FE00 (UTF-8 encoding E2 88 85 EF B8 80), where U+2205 is the
expected Unicode point for "EMPTY SET".
This variation selector is difficult to work with in CoqIDE. If some
notation is defined to expect a U+2205 symbol, then a U+2205 U+FE00
expression does not match that notation, even though it is visually
identical. As a concrete example, this makes it difficult to use CoqIDE
to type the U+2205 EMPTY SET symbol for use with Iris, which expects a
U+2205 without a U+FE00. Pressing "backspace" at the right point deletes
the U+FE00 variation selector, even though visually nothing appears to
happen, which is also confusing.
This commit removes the U+FE00 invisible variation selectors from any
symbols in the default bindings for CoqIDE (it appeared in 35 symbols
out of 1400+ symbols; I have no theory for why those 35 symbols were
special in this way). This change was generated using:
sed -e s,$(printf '\xef\xb8\x80'),,
| -rw-r--r-- | ide/default_bindings_src.ml | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/ide/default_bindings_src.ml b/ide/default_bindings_src.ml index 85a635a50f..a69a7c2aba 100644 --- a/ide/default_bindings_src.ml +++ b/ide/default_bindings_src.ml @@ -545,7 +545,7 @@ let bindings_set_1 = [ ["\\Hopf"; "\\quaternions" ], "ℍ", [letter]; ["\\planckh" ], "ℎ", [letter]; ["\\hslash"; "\\plankv" ], "ℏ", [letter]; - ["\\hbar"; "\\planck" ], "ℏ︀", [letter]; + ["\\hbar"; "\\planck" ], "ℏ", [letter]; ["\\Iscr"; "\\imagline" ], "ℐ", [letter]; ["\\Im"; "\\Ifr"; "\\image"; "\\imagpart" ], "ℑ", [letter]; ["\\Lscr"; "\\lagran"; "\\Laplacetrf" ], "ℒ", [letter]; @@ -1108,7 +1108,7 @@ let bindings_set_1 = [ ["\\isins" ], "⋴", [set]; ["\\isindot" ], "⋵", [set]; ["\\notinvc" ], "⋶", [set]; - ["\\notindot" ], "⋶︀", [set]; + ["\\notindot" ], "⋶", [set]; ["\\notinvb" ], "⋷", [set]; ["\\isinE" ], "⋹", [set]; ["\\nisd" ], "⋺", [set]; @@ -1192,40 +1192,40 @@ let bindings_set_1 = [ (* }}} *) (* {{{ Missing font *) - ["\\NegativeThickSpace" ], " ︀", [miscellanea]; - ["\\NegativeThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeVeryThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeMediumSpace" ], " ︀", [miscellanea]; - ["\\slarr"; "\\ShortLeftArrow" ], "←︀", [miscellanea]; - ["\\srarr"; "\\ShortRightArrow" ], "→︀", [miscellanea]; - ["\\empty"; "\\emptyset" ], "∅︀", [miscellanea]; - ["\\ssetmn"; "\\smallsetminus" ], "∖︀", [miscellanea]; - ["\\smid"; "\\shortmid" ], "∣︀", [miscellanea]; - ["\\nsmid"; "\\nshortmid" ], "∤︀", [miscellanea]; - ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥︀", [miscellanea]; - ["\\nparsl" ], "∥︀⃥", [miscellanea]; - ["\\nspar"; "\\nshortparallel" ], "∦︀", [miscellanea]; - ["\\caps" ], "∩︀", [miscellanea]; - ["\\cups" ], "∪︀", [miscellanea]; - ["\\thksim"; "\\thicksim" ], "∼︀", [miscellanea]; - ["\\thkap"; "\\thickapprox" ], "≈︀", [miscellanea]; - ["\\nedot" ], "≠︀", [miscellanea]; + ["\\NegativeThickSpace" ], " ", [miscellanea]; + ["\\NegativeThinSpace" ], " ", [miscellanea]; + ["\\NegativeVeryThinSpace" ], " ", [miscellanea]; + ["\\NegativeMediumSpace" ], " ", [miscellanea]; + ["\\slarr"; "\\ShortLeftArrow" ], "←", [miscellanea]; + ["\\srarr"; "\\ShortRightArrow" ], "→", [miscellanea]; + ["\\empty"; "\\emptyset" ], "∅", [miscellanea]; + ["\\ssetmn"; "\\smallsetminus" ], "∖", [miscellanea]; + ["\\smid"; "\\shortmid" ], "∣", [miscellanea]; + ["\\nsmid"; "\\nshortmid" ], "∤", [miscellanea]; + ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥", [miscellanea]; + ["\\nparsl" ], "∥⃥", [miscellanea]; + ["\\nspar"; "\\nshortparallel" ], "∦", [miscellanea]; + ["\\caps" ], "∩", [miscellanea]; + ["\\cups" ], "∪", [miscellanea]; + ["\\thksim"; "\\thicksim" ], "∼", [miscellanea]; + ["\\thkap"; "\\thickapprox" ], "≈", [miscellanea]; + ["\\nedot" ], "≠", [miscellanea]; ["\\bnequiv" ], "≡⃥", [miscellanea]; - ["\\lvnE"; "\\lvertneqq" ], "≨︀", [miscellanea]; - ["\\gvnE"; "\\gvertneqq" ], "≩︀", [miscellanea]; - ["\\nLtv"; "\\NotLessLess" ], "≪̸︀", [miscellanea]; - ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸︀", [miscellanea]; + ["\\lvnE"; "\\lvertneqq" ], "≨", [miscellanea]; + ["\\gvnE"; "\\gvertneqq" ], "≩", [miscellanea]; + ["\\nLtv"; "\\NotLessLess" ], "≪̸", [miscellanea]; + ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸", [miscellanea]; ["\\nle"; "\\NotLessEqual" ], "≰⃥", [miscellanea]; ["\\nge"; "\\NotGreaterEqual" ], "≱⃥", [miscellanea]; - ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊︀", [miscellanea]; - ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋︀", [miscellanea]; - ["\\sqcaps" ], "⊓︀", [miscellanea]; - ["\\sqcups" ], "⊔︀", [miscellanea]; + ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊", [miscellanea]; + ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋", [miscellanea]; + ["\\sqcaps" ], "⊓", [miscellanea]; + ["\\sqcups" ], "⊔", [miscellanea]; ["\\prurel" ], "⊰", [miscellanea]; - ["\\lesg" ], "⋚︀", [miscellanea]; - ["\\gesl" ], "⋛︀", [miscellanea]; - ["\\ShortUpArrow" ], "⌃︀", [miscellanea]; - ["\\ShortDownArrow" ], "⌄︀", [miscellanea]; + ["\\lesg" ], "⋚", [miscellanea]; + ["\\gesl" ], "⋛", [miscellanea]; + ["\\ShortUpArrow" ], "⌃", [miscellanea]; + ["\\ShortDownArrow" ], "⌄", [miscellanea]; ["\\target" ], "⌖", [miscellanea]; ["\\cylcty" ], "⌭", [miscellanea]; ["\\profalar" ], "⌮", [miscellanea]; @@ -1248,7 +1248,7 @@ let bindings_set_1 = [ ["\\ltrPar" ], "⦖", [miscellanea]; ["\\vzigzag" ], "⦚", [miscellanea]; ["\\angrtvbd" ], "⦝", [miscellanea]; - ["\\angrtvb" ], "⦝︀", [miscellanea]; + ["\\angrtvb" ], "⦝", [miscellanea]; ["\\ange" ], "⦤", [miscellanea]; ["\\range" ], "⦥", [miscellanea]; ["\\dwangle" ], "⦦", [miscellanea]; @@ -1367,9 +1367,9 @@ let bindings_set_1 = [ ["\\smt" ], "⪪", [miscellanea]; ["\\lat" ], "⪫", [miscellanea]; ["\\smte" ], "⪬", [miscellanea]; - ["\\smtes" ], "⪬︀", [miscellanea]; + ["\\smtes" ], "⪬", [miscellanea]; ["\\late" ], "⪭", [miscellanea]; - ["\\lates" ], "⪭︀", [miscellanea]; + ["\\lates" ], "⪭", [miscellanea]; ["\\Sc" ], "⪼", [miscellanea]; ["\\subdot" ], "⪽", [miscellanea]; ["\\supdot" ], "⪾", [miscellanea]; |
