From 50fe6429e852a78f8e870a4bfcb444f60cb0b7de Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 25 Sep 2018 13:34:44 +0200 Subject: latex to unicode in coqide --- ide/coqide.ml | 12 ++++++++- ide/coqide_ui.ml | 2 ++ ide/preferences.ml | 56 ++++++++++++++++++++++++++++++++++++------ ide/preferences.mli | 2 ++ ide/wg_ScriptView.ml | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++ ide/wg_ScriptView.mli | 1 + 6 files changed, 131 insertions(+), 9 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 94778e0c60..5e4994eeb8 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -453,7 +453,7 @@ let compile sn = |None -> flash_info "Active buffer has no name" |Some f -> let args = Coq.get_arguments sn.coqtop in - let cmd = cmd_coqc#get + let cmd = cmd_coqc#get ^ " " ^ String.concat " " args ^ " " ^ (Filename.quote f) ^ " 2>&1" in @@ -766,6 +766,14 @@ let about _ = dialog#set_authors authors; dialog#show () +let latex_to_unicode = + cb_on_current_term (fun t -> + (*let show_warning s = + t.messages#clear; + t.messages#add_string s + in*) + t.script#latex_to_unicode() (*show_warning*)) + let comment = cb_on_current_term (fun t -> t.script#comment ()) let uncomment = cb_on_current_term (fun t -> t.script#uncomment ()) @@ -1161,6 +1169,8 @@ let build_ui () = ~callback:MiscMenu.uncomment; item "Coqtop arguments" ~label:"Coqtop _arguments" ~callback:MiscMenu.coqtop_arguments; + item "Latex-to-unicode" ~label:"_Latex-to-unicode" ~accel:"space" + ~callback:MiscMenu.latex_to_unicode; ]; menu compile_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index c994898a4f..c30d6604d2 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -140,6 +140,8 @@ let init () = \n \ \n \ \n \ +\n \ +\n \ \n \ \n \ \n \ diff --git a/ide/preferences.ml b/ide/preferences.ml index fb0eea1405..a5b294cd3a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -28,6 +28,41 @@ type tag = { tag_strikethrough : bool; } + +(** Latex to unicode bindings. + + Text description of the unicode bindings, in a file coqide.bindings + one item per line, each item consists of: + - a leading backslahs + - a ascii word next to it + - a unicode word (or possibly a full sentence in-between doube-quotes, + the sentence may include spaces and \n tokens), + - optinally, an integer indicating the "priority" (lower is higher priority), + technically the length of the prefix that suffices to obtain this word. + Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda". + + \pi π + \lambda λ 3 + \lambdas λs 4 + \lake Ο 2 + \lemma "Lemma foo : x. Proof. Qed." 1 + + - In case of equality between two candidates (same ascii word, or same + priorities for two words with similar prefix), the first binding is considered. +*) + +let latex_to_unicode = ref + [ (* dummy default, used for testing *) + ("\\pi", "π", None); + ("\\lambdas", "λs", Some 4); + ("\\lambda", "λ", Some 3); + ("\\lake", "0", Some 2); + ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); + ] + +let get_latex_to_unicode () = + !latex_to_unicode + (** Generic preferences *) type obj = { @@ -248,6 +283,10 @@ let loaded_accel_file = try get_config_file "coqide.keys" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" +let loaded_unicode_file = + try get_config_file "coqide.bindings" + with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings" + (** Hooks *) (** New style preferences *) @@ -326,7 +365,7 @@ let modifier_for_navigation = let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"" ~repr:Repr.(string) - + let modifier_for_tactics = new preference ~name:["modifier_for_tactics"] ~init:"" ~repr:Repr.(string) @@ -643,14 +682,15 @@ let save_pref () = let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in + (* TODO: parse loaded_unicode_file and save it in reference latex_to_unicode *) - let m = Config_lexer.load_file loaded_pref_file in - let iter name v = - if Util.String.Map.mem name !preferences then - try (Util.String.Map.find name !preferences).set v with _ -> () - else unknown_preferences := Util.String.Map.add name v !unknown_preferences - in - Util.String.Map.iter iter m + let m = Config_lexer.load_file loaded_pref_file in + let iter name v = + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences + in + Util.String.Map.iter iter m let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get diff --git a/ide/preferences.mli b/ide/preferences.mli index cf2265781c..52303ea6cf 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -111,3 +111,5 @@ val stick : 'a preference -> (#GObj.widget as 'obj) -> ('a -> unit) -> unit val use_default_doc_url : string + +val get_latex_to_unicode : unit -> (string * string * int option) list diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 5e26c50797..e407c2a5d8 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -10,6 +10,8 @@ open Preferences +exception Abort + type insert_action = { ins_val : string; ins_off : int; @@ -405,6 +407,71 @@ object (self) self#buffer#delete_mark (`MARK stop_mark) | _ -> () + method latex_to_unicode () (* (show_warning:string->unit) *) = + let bindings = Preferences.get_latex_to_unicode() in + (** Auxiliary function to test whether [s] is a prefix of [str]; + Note that there might be overlap with wg_Completion::is_substring *) + let string_is_prefix s str = + let n = String.length s in + let m = String.length str in + if m < n + then false + else (s = String.sub str 0 n) + in + (* Auxiliary function to perform the lookup for a binding *) + let lookup prefix = (* lookup : string -> string option *) + let max_priority = 100000000 in + let cur_word = ref None in + let cur_prio = ref (max_priority+1) in + let test_binding (key, word, prio_opt) = + let prio = + match prio_opt with + | None -> max_priority + | Some p -> p + in + if string_is_prefix prefix key && prio < !cur_prio then begin + cur_word := Some word; + cur_prio := prio; + end in + List.iter test_binding bindings; + !cur_word + in + (** Auxiliary, copy-paste from method [comment] above; + btw, isn't there a more efficient way to achieve this? *) + let rec get_line_start iter = + if iter#starts_line then iter + else get_line_start iter#backward_char + in + let buffer = self#buffer in + let insert = buffer#get_iter `INSERT in + let insert_mark = buffer#create_mark ~left_gravity:false insert in + let () = buffer#begin_user_action () in + begin try + let line_start = get_line_start insert in + let prev_backslash_search = insert#backward_search ~limit:line_start "\\" in + let backslash = + match prev_backslash_search with + | None -> raise Abort + | Some (backslash_start,backslash_stop) -> backslash_start + in + let prefix = backslash#get_text ~stop:insert in + let word = + match lookup prefix with + | None -> + (* show_warning ("No binding match " ^ prefix); *) + raise Abort + | Some word -> word + in + let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in + if not was_deleted then raise Abort; + let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in + let _was_inserted = buffer#insert_interactive ~iter:insert2 word in + () + with Abort -> () end; + let () = self#buffer#end_user_action () in + self#buffer#delete_mark (`MARK insert_mark) + + method complete_popup = popup method undo = undo_manager#undo diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index be6510dbe2..eb1beedfad 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -26,6 +26,7 @@ object method set_show_right_margin : bool -> unit method comment : unit -> unit method uncomment : unit -> unit + method latex_to_unicode : unit -> unit (* (string -> unit) -> unit *) method recenter_insert : unit method complete_popup : Wg_Completion.complete_popup end -- cgit v1.2.3 From d183e6b3bef905032333135849104fc66d5de68d Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 25 Sep 2018 18:46:29 +0200 Subject: working set of bindings --- ide/default.bindings | 1156 ++++++++++++++++++++++++++++++++++++++++++++++++++ ide/preferences.ml | 35 +- ide/wg_ScriptView.ml | 53 +-- 3 files changed, 1215 insertions(+), 29 deletions(-) create mode 100644 ide/default.bindings diff --git a/ide/default.bindings b/ide/default.bindings new file mode 100644 index 0000000000..ac4d32fb34 --- /dev/null +++ b/ide/default.bindings @@ -0,0 +1,1156 @@ +\!' ¡ +\` ‘ +\`` “ +\' ′ +\'' ″ +\''' ‴ +\mbox'' ” +\mbox' ’ +\-- – +\--- — +\"A Ä +\"E Ë +\"H Ḧ +\"I Ï +\"O Ö +\"U Ü +\"W Ẅ +\"X Ẍ +\"Y Ÿ +\"a ä +\"e ë +\"h ḧ +\"i ï +\"o ö +\"t ẗ +\"u ü +\"w ẅ +\"x ẍ +\"y ÿ +\'A Á +\'C Ć +\'E É +\'G Ǵ +\'I Í +\'K Ḱ +\'L Ĺ +\'M Ḿ +\'N Ń +\'O Ó +\'P Ṕ +\'R Ŕ +\'S Ś +\'U Ú +\'W Ẃ +\'Y Ý +\'Z Ź +\'a á +\'c ć +\'e é +\'g ǵ +\'i í +\'k ḱ +\'l ĺ +\'m ḿ +\'n ń +\'o ó +\'p ṕ +\'r ŕ +\'s ś +\'u ú +\'w ẃ +\'y ý +\'z ź +\.A Ȧ +\.B Ḃ +\.C Ċ +\.D Ḋ +\.E Ė +\.F Ḟ +\.G Ġ +\.H Ḣ +\.I İ +\.M Ṁ +\.N Ṅ +\.O Ȯ +\.P Ṗ +\.R Ṙ +\.S Ṡ +\.T Ṫ +\.W Ẇ +\.X Ẋ +\.Y Ẏ +\.Z Ż +\.a ȧ +\.b ḃ +\.c ċ +\.d ḋ +\.e ė +\.f ḟ +\.g ġ +\.h ḣ +\.m ṁ +\.n ṅ +\.o ȯ +\.p ṗ +\.r ṙ +\.s ṡ +\.t ṫ +\.w ẇ +\.x ẋ +\.y ẏ +\.z ż +\=A Ā +\=E Ē +\=G Ḡ +\=I Ī +\=O Ō +\=U Ū +\=Y Ȳ +\=a ā +\=e ē +\=g ḡ +\=i ī +\=o ō +\=u ū +\=y ȳ +\AA Å +\AE Æ +\Alpha Α 1 +\Beta Β 1 +\Box □ +\Bumpeq ≎ +\Cap ⋒ +\Chi Χ 1 +\Cup ⋓ +\DH Ð +\Delta Δ 1 +\Diamond ◇ +\Downarrow ⇓ +\Epsilon Ε 1 +\Eta Η 1 +\Finv Ⅎ +\Gamma Γ 1 +\Im ℑ +\Join ⋈ +\Kappa Κ 1 +\L Ł +\Lambda Λ 1 +\Leftarrow ⇐ +\Leftrightarrow ⇔ +\Lleftarrow ⇚ +\Longleftarrow ⇐ +\Longleftrightarrow ⇔ +\Longrightarrow ⇒ +\Lsh ↰ +\Mu Μ 1 +\Nu Ν 1 +\O Ø +\OE Œ +\Omega Ω +\W Ω 1 +\Omicron Ο 1 +\P ¶ +\Phi Φ +\F Φ 1 +\Pi Π 1 +\Psi Ψ +\Re ℜ +\Rho Ρ 1 +\Rightarrow ⇒ +\Rrightarrow ⇛ +\Rsh ↱ +\S § +\Sigma Σ 1 +\Subset ⋐ +\Supset ⋑ +\TH Þ +\Tau Τ 1 +\Theta Θ 1 +\Uparrow ⇑ +\Updownarrow ⇕ +\Upsilon Υ 1 +\Vdash ⊩ +\Vvdash ⊪ +\Xi Ξ 1 +\Zeta Ζ 1 +\^A  +\^C Ĉ +\^E Ê +\^G Ĝ +\^H Ĥ +\^I Î +\^J Ĵ +\^O Ô +\^S Ŝ +\^U Û +\^W Ŵ +\^Y Ŷ +\^Z Ẑ +\^a â +\^c ĉ +\^e ê +\^g ĝ +\^h ĥ +\^i î +\^j ĵ +\^o ô +\^s ŝ +\^u û +\^w ŵ +\^y ŷ +\^z ẑ +\`A À +\`E È +\`I Ì +\`N Ǹ +\`O Ò +\`U Ù +\`W Ẁ +\`Y Ỳ +\`a à +\`e è +\`i ì +\`n ǹ +\`o ò +\`u ù +\`w ẁ +\`y ỳ +\aa å +\ae æ +\aleph ℵ +\alpha α 1 +\angle ∠ +\approx ≈ +\approxeq ≊ +\aquarius ♒ +\aries ♈ +\ascnode ☊ +\ast ∗ +\astrosun ☉ +\asymp ≍ +\backepsilon ∍ +\backprime ‵ +\backsim ∽ +\barwedge ⊼ +\barA Ā +\barE Ē +\barG Ḡ +\barI Ī +\barO Ō +\barU Ū +\barY Ȳ +\bara ā +\bare ē +\barg ḡ +\bari ī +\baro ō +\baru ū +\bary ȳ +\because ∵ +\beta β 1 +\beth ℶ +\between ≬ +\bigcap ⋂ +\bigcirc ○ +\bigcup ⋃ +\bigodot ⊙ +\bigoplus ⊕ +\bigotimes ⊗ +\bigsqcup ⊔ +\bigstar ★ +\bigtriangledown ▽ +\bigtriangleup △ +\biguplus ⊎ +\bigvee ⋁ +\bigwedge ⋀ +\blackbishop ♝ +\blackking ♚ +\blackknight ♞ +\blacklozenge ◆ +\blackpawn ♟ +\blackqueen ♛ +\blackrook ♜ +\blacksquare ■ +\blacktriangle ▲ +\blacktriangledown ▼ +\blacktriangleleft ◀ +\blacktriangleright ▷ +\bot ⊥ +\bowtie ⋈ +\boxdot ⊡ +\boxminus ⊟ +\boxplus ⊞ +\boxtimes ⊠ +\breveA Ă +\breveE Ĕ +\breveG Ğ +\breveI Ĭ +\breveO Ŏ +\breveU Ŭ +\brevea ă +\brevee ĕ +\breveg ğ +\brevei ĭ +\breveo ŏ +\breveu ŭ +\bullet ∙ +\bumpeq ≏ +\cancer ♋ +\cap ∩ +\capricornus ♑ +\capslockkey ⇪ +\cdot ⋅ +\cdots ⋯ +\centerdot ⋅ +\cents ¢ +\checkA Ǎ +\checkC Č +\checkD Ď +\checkE Ě +\checkN Ň +\checkR Ř +\checkS Š +\checkT Ť +\checkZ Ž +\checka ǎ +\checkc č +\checkd ď +\checke ě +\checkn ň +\checkr ř +\checks š +\checkt ť +\checkz ž +\chi χ 1 +\circ ∘ +\circeq ≗ +\circlearrowleft ↺ +\circlearrowright ↻ +\circledS Ⓢ +\circledast ⊛ +\circledcirc ⊚ +\circleddash ⊝ +\clubsuit ♣ +\cmdkey ⌘ +\complement ∁ +\cong ≅ +\conjunction ☌ +\coprod ∐ +\copyright © +\cup ∪ +\curlyeqprec ⋞ +\curlyeqsucc ⋟ +\curlyvee ⋎ +\curlywedge ⋏ +\curvearrowleft ↶ +\curvearrowright ↷ +\cC Ç +\cc ç +\dag † +\dagger † +\daleth ℸ +\dashleftarrow ⇠ +\dashrightarrow ⇢ +\dashv ⊣ +\ddag ‡ +\ddagger ‡ +\ddots ⋱ +\ddotA Ä +\ddotE Ë +\ddotH Ḧ +\ddotI Ï +\ddotO Ö +\ddotU Ü +\ddotW Ẅ +\ddotX Ẍ +\ddotY Ÿ +\ddota ä +\ddote ë +\ddoth ḧ +\ddoti ï +\ddoto ö +\ddott ẗ +\ddotu ü +\ddotw ẅ +\ddotx ẍ +\ddoty ÿ +\degree ° +\delkey ⌫ +\delta δ 1 +\descnode ☋ +\dh ð +\diamond ⋄ +\diamondsuit ♢ +\digamma Ϝ +\div ÷ +\divideontimes ⋇ +\doteq ≐ +\doteqdot ≑ +\dotplus ∔ +\dotA Ȧ +\dotB Ḃ +\dotC Ċ +\dotD Ḋ +\dotE Ė +\dotF Ḟ +\dotG Ġ +\dotH Ḣ +\dotI İ +\dotM Ṁ +\dotN Ṅ +\dotO Ȯ +\dotP Ṗ +\dotR Ṙ +\dotS Ṡ +\dotT Ṫ +\dotW Ẇ +\dotX Ẋ +\dotY Ẏ +\dotZ Ż +\dota ȧ +\dotb ḃ +\dotc ċ +\dotd ḋ +\dote ė +\dotf ḟ +\dotg ġ +\doth ḣ +\dotm ṁ +\dotn ṅ +\doto ȯ +\dotp ṗ +\dotr ṙ +\dots ṡ +\dott ṫ +\dotw ẇ +\dotx ẋ +\doty ẏ +\dotz ż +\downarrow ↓ +\downdownarrows ⇊ +\downharpoonleft ⇃ +\downharpoonright ⇂ +\dA Ạ +\dB Ḅ +\dD Ḍ +\dE Ẹ +\dH Ḥ +\dI Ị +\dK Ḳ +\dL Ḷ +\dM Ṃ +\dN Ṇ +\dO Ọ +\dR Ṛ +\dS Ṣ +\dT Ṭ +\dU Ụ +\dV Ṿ +\dW Ẉ +\dY Ỵ +\dZ Ẓ +\da ạ +\db ḅ +\dd ḍ +\de ẹ +\dh ḥ +\di ị +\dk ḳ +\dl ḷ +\dm ṃ +\dn ṇ +\do ọ +\dr ṛ +\ds ṣ +\dt ṭ +\du ụ +\dv ṿ +\dw ẉ +\dy ỵ +\dz ẓ +\earth ⊕ +\ejectkey ⏏ +\ell ℓ +\emptyset ∅ +\enterkey ⌤ +\epsdice1 ⚀ +\epsdice2 ⚁ +\epsdice3 ⚂ +\epsdice4 ⚃ +\epsdice5 ⚄ +\epsdice6 ⚅ +\epsilon ∊ +\eqcirc ≖ +\equiv ≡ +\esckey ⎋ +\eta η 1 +\eth ð +\euro € +\exists ∃ +\fallingdotseq ≒ +\flat ♭ +\forall ∀ +\frown ⌢ +\gamma γ 1 +\ge ≥ +\gemini ♊ +\geq ≥ +\geqq ≧ +\gg ≫ +\ggg ⋙ +\gimel ℷ +\gtrdot ⋗ +\gtreqless ⋛ +\gtrless ≷ +\gtrsim ≳ +\hbar ℏ +\heartsuit ♡ +\hookleftarrow ↩ +\hookrightarrow ↪ +\hslash ℏ +\iiiint ⨌ +\iiint ∭ +\iint ∬ +\implies ⇒ +\in ∈ +\infty ∞ +\int ∫ +\intercal ⊺ +\iota ι 1 +\jupiter ♃ +\kappa κ 1 +\l{} ł +\lambda λ 1 +\langle ⟨ +\lceil ⌈ +\ldots … +\le ≤ +\leadsto ↝ +\leftarrow ← +\leftarrowtail ↢ +\leftharpoondown ↽ +\leftharpoonup ↼ +\leftleftarrows ⇇ +\leftmoon ☾ +\leftrightarrow ↔ +\leftrightarrows ⇆ +\leftrightharpoons ⇋ +\leftrightsquigarrow ↭ +\leftthreetimes ⋋ +\leo ♌ +\leq ≤ +\leqq ≦ +\leqslant ≤ +\lessdot ⋖ +\lesseqgtr ⋚ +\lessgtr ≶ +\lesssim ≲ +\lfloor ⌊ +\lhd ⊲ +\libra ♎ +\ll ≪ +\lll ⋘ +\longleftarrow ← +\longleftrightarrow ↔ +\longmapsto ⇖ +\longrightarrow → +\looparrowleft ↫ +\looparrowright ↬ +\lozenge ◊ +\ltimes ⋉ +\mapsto ↦ +\mars ♂ +\bb0 𝟘 +\bb1 𝟙 +\bb2 𝟚 +\bb3 𝟛 +\bb4 𝟜 +\bb5 𝟝 +\bb6 𝟞 +\bb7 𝟟 +\bb8 𝟠 +\bb9 𝟡 +\bbA 𝔸 +\bbB 𝔹 +\bbC ℂ +\bbD 𝔻 +\bbE 𝔼 +\bbF 𝔽 +\bbG 𝔾 +\bbH ℍ +\bbI 𝕀 +\bbJ 𝕁 +\bbK 𝕂 +\bbL 𝕃 +\bbM 𝕄 +\bbN ℕ +\bbO 𝕆 +\bbP ℙ +\bbQ ℚ +\bbR ℝ +\bbS 𝕊 +\bbT 𝕋 +\bbU 𝕌 +\bbV 𝕍 +\bbW 𝕎 +\bbX 𝕏 +\bbY 𝕐 +\bbZ ℤ +\bba 𝕒 +\bbb 𝕓 +\bbc 𝕔 +\bbd 𝕕 +\bbe 𝕖 +\bbf 𝕗 +\bbg 𝕘 +\bbh 𝕙 +\bbi 𝕚 +\bbj 𝕛 +\bbk 𝕜 +\bbl 𝕝 +\bbm 𝕞 +\bbn 𝕟 +\bbo 𝕠 +\bbp 𝕡 +\bbq 𝕢 +\bbr 𝕣 +\bbs 𝕤 +\bbt 𝕥 +\bbu 𝕦 +\bbv 𝕧 +\bbw 𝕨 +\bbx 𝕩 +\bby 𝕪 +\bbz 𝕫 +\calA 𝒜 +\calB ℬ +\calC 𝒞 +\calD 𝒟 +\calE ℰ +\calF ℱ +\calG 𝒢 +\calH ℋ +\calI ℐ +\calJ 𝒥 +\calK 𝒦 +\calL ℒ +\calM ℳ +\calN 𝒩 +\calO 𝒪 +\calP 𝒫 +\calQ 𝒬 +\calR ℛ +\calS 𝒮 +\calT 𝒯 +\calU 𝒰 +\calV 𝒱 +\calW 𝒲 +\calX 𝒳 +\calY 𝒴 +\calZ 𝒵 +\cala 𝒶 +\calb 𝒷 +\calc 𝒸 +\cald 𝒹 +\cale ℯ +\calf 𝒻 +\calg ℊ +\calh 𝒽 +\cali 𝒾 +\calj 𝒿 +\calk 𝓀 +\call 𝓁 +\calm 𝓂 +\caln 𝓃 +\calo ℴ +\calp 𝓅 +\calq 𝓆 +\calr 𝓇 +\cals 𝓈 +\calt 𝓉 +\calu 𝓊 +\calv 𝓋 +\calw 𝓌 +\calx 𝓍 +\caly 𝓎 +\calz 𝓏 +\frakA 𝔄 +\frakB 𝔅 +\frakC ℭ +\frakD 𝔇 +\frakE 𝔈 +\frakF 𝔉 +\frakG 𝔊 +\frakH ℌ +\frakI ℑ +\frakJ 𝔍 +\frakK 𝔎 +\frakL 𝔏 +\frakM 𝔐 +\frakN 𝔑 +\frakO 𝔒 +\frakP 𝔓 +\frakQ 𝔔 +\frakR ℜ +\frakS 𝔖 +\frakT 𝔗 +\frakU 𝔘 +\frakV 𝔙 +\frakW 𝔚 +\frakX 𝔛 +\frakY 𝔜 +\frakZ ℨ +\fraka 𝔞 +\frakb 𝔟 +\frakc 𝔠 +\frakd 𝔡 +\frake 𝔢 +\frakf 𝔣 +\frakg 𝔤 +\frakh 𝔥 +\fraki 𝔦 +\frakj 𝔧 +\frakk 𝔨 +\frakl 𝔩 +\frakm 𝔪 +\frakn 𝔫 +\frako 𝔬 +\frakp 𝔭 +\frakq 𝔮 +\frakr 𝔯 +\fraks 𝔰 +\frakt 𝔱 +\fraku 𝔲 +\frakv 𝔳 +\frakw 𝔴 +\frakx 𝔵 +\fraky 𝔶 +\frakz 𝔷 +\measuredangle ∡ +\mercury ☿ +\mho ℧ +\mid ∣ +\models ⊨ +\mp ∓ +\mu μ 1 +\multimap ⊸ +\nabla ∇ +\natural ♮ +\nearrow ↗ +\neg ¬ +\neptune ♆ +\neq ≠ +\nexists ∄ +\ng ŋ +\ni ∋ +\not< ≮ +\not> ≯ +\not\Vdash ⊮ +\not\approx ≉ +\not\cong ≇ +\not\equiv ≢ +\not\ge ≱ +\not\gtrless ≹ +\not\in ∉ +\not\le ≰ +\not\models ⊭ +\not\ni ∌ +\not\sim ≄ +\not\sqsubseteq ⋢ +\not\sqsupseteq ⋣ +\not\subset ⊄ +\not\subseteq ⊈ +\not\supset ⊅ +\not\supseteq ⊉ +\not\vdash ⊬ +\notin ∉ +\nu ν 1 +\v ν 1 +\nwarrow ↖ +\o{} ø +\odot ⊙ +\oe œ +\oint ∮ +\omega ω +\w ω 1 +\omicron ο 1 +\ominus ⊖ +\oplus ⊕ +\opposition ☍ +\optkey ⌥ +\oslash ⊘ +\otimes ⊗ +\parallel ∥ +\partial ∂ +\perp ⊥ +\phi φ +\f φ 1 +\pi π 1 +\pilcrow ¶ +\pisces ♓ +\pitchfork ⋔ +\pluto ♇ +\pm ± +\pound £ +\pounds £ +\prec ≺ +\preccurlyeq ≼ +\preceq ≼ +\precsim ≾ +\prime ′ +\prod ∏ +\propto ∝ +\psi ψ +\rangle ⟩ +\rceil ⌉ +\registered ® +\returnkey ⏎ +\revtabkey ⇤ +\rfloor ⌋ +\rhd ⊳ +\rho ρ 1 +\rightarrow → +\rightarrowtail ↣ +\rightdelkey ⌦ +\rightharpoondown ⇁ +\rightharpoonup ⇀ +\rightleftarrows ⇄ +\rightleftharpoons ⇌ +\rightmoon ☽ +\rightrightarrows ⇉ +\rightsquigarrow ⇝ +\rightthreetimes ⋌ +\risingdotseq ≓ +\rtimes ⋊ +\sagittarius ♐ +\saturn ♄ +\scorpio ♏ +\searrow ↘ +\section § +\setminus ∖ +\sharp ♯ +\shiftkey ⇧ +\shortparallel ∥ +\sigma σ 1 +\sim ∼ +\simeq ≃ +\smallfrown ⌢ +\smallsetminus ∖ +\smallsmile ⌣ +\smile ⌣ +\space ␣ +\spadesuit ♠ +\sphericalangle ∢ +\sqcap ⊓ +\sqcup ⊔ +\sqsubset ⊏ +\sqsubseteq ⊑ +\sqsupset ⊐ +\sqsupseteq ⊒ +\square □ +\ss ß +\star ⋆ +\subset ⊂ +\subseteq ⊆ +\subsetneq ⊊ +\succ ≻ +\succcurlyeq ≽ +\succeq ≽ +\succsim ≿ +\sum ∑ +\supset ⊃ +\supseteq ⊇ +\supsetneq ⊋ +\surd √ +\swarrow ↙ +\tabkey ⇥ +\tau τ 1 +\taurus ♉ +\textbabygamma ɤ +\textbarglotstop ʡ +\textbari ɨ +\textbaro ɵ +\textbarrevglotstop ʢ +\textbaru ʉ +\textbeltl ɬ +\textbeta β +\textbullseye ʘ +\textchi χ +\textcloserevepsilon ɞ +\textcrh ħ +\textctc ɕ +\textctj ʝ +\textctz ʑ +\textdoublepipe ǁ +\textdyoghlig ʤ +\textepsilon ɛ +\textesh ʃ +\textfishhookr ɾ +\textgamma ɣ +\textglotstop ʔ +\textgrgamma γ +\texthtb ɓ +\texthtd ɗ +\texthtg ɠ +\texthth ɦ +\texththeng ɧ +\texthtscg ʛ +\textinvscr ʁ +\textiota ι +\textltailm ɱ +\textltailn ɲ +\textltilde ɫ +\textlyoghlig ɮ +\textopeno ɔ +\textphi ɸ +\textpipe ǀ +\textregistered ® +\textreve ɘ +\textrevepsilon ɜ +\textrevglotstop ʕ +\textrhookrevepsilon ɝ +\textrighthookschwa ɚ +\textrtaild ɖ +\textrtaill ɭ +\textrtailn ɳ +\textrtailr ɽ +\textrtails ʂ +\textrtailt ʈ +\textrtailz ʐ +\textscb ʙ +\textscg ɢ +\textsch ʜ +\textschwa ə +\textsci ɪ +\textscl ʟ +\textscn ɴ +\textscoelig ɶ +\textscr ʀ +\textscripta ɑ +\textscriptv ʋ +\textscy ʏ +\textteshlig ʧ +\texttheta θ +\texttrademark ™ +\textturna ɐ +\textturnh ɥ +\textturnlonglegr ɺ +\textturnm ɯ +\textturnmrleg ɰ +\textturnr ɹ +\textturnrrtail ɻ +\textturnscripta ɒ +\textturnv ʌ +\textturnw ʍ +\textturny ʎ +\textupsilon ʊ +\textyogh ʒ +\th þ +\therefore ∴ +\theta θ 1 +\h θ 1 +\thickapprox ≈ +\thicksim ∼ +\times × +\top ⊤ +\trademark ™ +\triangle △ +\triangledown ▽ +\triangleleft ◁ +\trianglelefteq ⊴ +\triangleq ≜ +\triangleright ▷ +\trianglerighteq ⊵ +\twoheadleftarrow ↞ +\twoheadrightarrow ↠ +\unlhd ⊴ +\unrhd ⊵ +\uparrow ↑ +\updownarrow ↕ +\upharpoonleft ↿ +\upharpoonright ↾ +\uplus ⊎ +\upsilon υ 1 +\upuparrows ⇈ +\uranus ⛢ +\uA Ă +\uE Ĕ +\uG Ğ +\uI Ĭ +\uO Ŏ +\uU Ŭ +\ua ă +\ue ĕ +\ug ğ +\ui ĭ +\uo ŏ +\uu ŭ +\vDash ⊨ +\varepsilon ε +\varkappa ϰ +\varnothing ∅ +\varphi ϕ +\varpi ϖ +\varpropto ∝ +\varrho ϱ +\varsigma ς +\vartheta ϑ +\vartriangle △ +\vartriangleleft ⊲ +\vartriangleright ⊳ +\vdash ⊢ +\vdots ⋮ +\vee ∨ +\veebar ⊻ +\venus ♀ +\virgo ♍ +\vA Ǎ +\vC Č +\vD Ď +\vE Ě +\vN Ň +\vR Ř +\vS Š +\vT Ť +\vZ Ž +\va ǎ +\vc č +\vd ď +\ve ě +\vn ň +\vr ř +\vs š +\vt ť +\vz ž +\wedge ∧ +\whitebishop ♗ +\whiteking ♔ +\whiteknight ♘ +\whitepawn ♙ +\whitequeen ♕ +\whiterook ♖ +\wp ℘ +\wr ≀ +\xi ξ +\zeta ζ 1 +\~A Ā +\~E Ẽ +\~I Ĩ +\~N Ñ +\~O Õ +\~U Ũ +\~Y Ỹ +\~a ã +\~e ẽ +\~i ĩ +\~n ñ +\~o õ +\~u ũ +\~y ỹ +\^( ⁽ +\^) ⁾ +\^+ ⁺ +\^- ⁻ +\^0 ⁰ +\^1 ¹ +\^2 ² +\^3 ³ +\^4 ⁴ +\^5 ⁵ +\^6 ⁶ +\^7 ⁷ +\^8 ⁸ +\^9 ⁹ +\^= ⁼ +\^A ᴬ +\^B ᴮ +\^D ᴰ +\^E ᴱ +\^G ᴳ +\^H ᴴ +\^I ᴵ +\^J ᴶ +\^K ᴷ +\^L ᴸ +\^M ᴹ +\^N ᴺ +\^O ᴼ +\^P ᴾ +\^R ᴿ +\^T ᵀ +\^U ᵁ +\^V ⱽ +\^W ᵂ +\^alpha ᵅ +\^beta ᵝ +\^chi ᵡ +\^delta ᵟ +\^epsilon ᵋ +\^gamma ᵞ +\^iota ᶥ +\^phi ᶲ +\^theta ᶿ +\^varphi ᵠ +\^a ᵃ +\^b ᵇ +\^c ᶜ +\^d ᵈ +\^e ᵉ +\^f ᶠ +\^g ᵍ +\^h ʰ +\^i ⁱ +\^j ʲ +\^k ᵏ +\^l ˡ +\^m ᵐ +\^n ⁿ +\^o ᵒ +\^p ᵖ +\^r ʳ +\^s ˢ +\^t ᵗ +\^u ᵘ +\^v ᵛ +\^w ʷ +\^x ˣ +\^y ʸ +\^z ᶻ +\_( ₍ +\_) ₎ +\_+ ₊ +\_- ₋ +\_0 ₀ +\_1 ₁ +\_2 ₂ +\_3 ₃ +\_4 ₄ +\_5 ₅ +\_6 ₆ +\_7 ₇ +\_8 ₈ +\_9 ₉ +\_= ₌ +\_beta ᵦ +\_chi ᵪ +\_gamma ᵧ +\_rho ᵨ +\_varphi ᵩ +\_a ₐ +\_e ₑ +\_h ₕ +\_i ᵢ +\_j ⱼ +\_k ₖ +\_l ₗ +\_m ₘ +\_n ₙ +\_o ₒ +\_p ₚ +\_r ᵣ +\_s ₛ +\_t ₜ +\_u ᵤ +\_v ᵥ +\_x ₓ diff --git a/ide/preferences.ml b/ide/preferences.ml index a5b294cd3a..2701089331 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -51,18 +51,45 @@ type tag = { priorities for two words with similar prefix), the first binding is considered. *) -let latex_to_unicode = ref - [ (* dummy default, used for testing *) +let latex_to_unicode = ref [] + (* dummy default, used for testing + [ ("\\pi", "π", None); ("\\lambdas", "λs", Some 4); ("\\lambda", "λ", Some 3); ("\\lake", "0", Some 2); ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] + *) let get_latex_to_unicode () = !latex_to_unicode +let load_latex_to_unicode_file filename = + let acc = ref [] in + let ch = open_in filename in + begin try while true do + let line = input_line ch in + begin try + let chline = Scanf.Scanning.from_string line in + let (key,value) = + Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in + let prio = + try Scanf.bscanf chline " %d" (fun x -> Some x) + with Scanf.Scan_failure _ | Failure _ | End_of_file -> None + in + acc := (key,value,prio)::!acc; + Scanf.Scanning.close_in chline; + with End_of_file -> () end; + done with End_of_file -> () end; + close_in ch; + latex_to_unicode := List.rev !acc + (*List.iter (fun (x,y,p) -> + Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) + !latex_to_unicode; + prerr_newline() *) + + (** Generic preferences *) type obj = { @@ -283,7 +310,7 @@ let loaded_accel_file = try get_config_file "coqide.keys" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" -let loaded_unicode_file = +let loaded_bindings_file = try get_config_file "coqide.bindings" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings" @@ -682,7 +709,7 @@ let save_pref () = let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - (* TODO: parse loaded_unicode_file and save it in reference latex_to_unicode *) + let () = load_latex_to_unicode_file loaded_bindings_file in let m = Config_lexer.load_file loaded_pref_file in let iter name v = diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index e407c2a5d8..97bf9aefc5 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -436,38 +436,41 @@ object (self) List.iter test_binding bindings; !cur_word in - (** Auxiliary, copy-paste from method [comment] above; - btw, isn't there a more efficient way to achieve this? *) + (** Auxiliary method to reach the beginning of line or the + nearest space before the iterator. *) let rec get_line_start iter = - if iter#starts_line then iter + if iter#starts_line || Glib.Unichar.isspace iter#char then iter else get_line_start iter#backward_char in + (** Main action *) let buffer = self#buffer in let insert = buffer#get_iter `INSERT in let insert_mark = buffer#create_mark ~left_gravity:false insert in let () = buffer#begin_user_action () in - begin try - let line_start = get_line_start insert in - let prev_backslash_search = insert#backward_search ~limit:line_start "\\" in - let backslash = - match prev_backslash_search with - | None -> raise Abort - | Some (backslash_start,backslash_stop) -> backslash_start - in - let prefix = backslash#get_text ~stop:insert in - let word = - match lookup prefix with - | None -> - (* show_warning ("No binding match " ^ prefix); *) - raise Abort - | Some word -> word - in - let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in - if not was_deleted then raise Abort; - let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in - let _was_inserted = buffer#insert_interactive ~iter:insert2 word in - () - with Abort -> () end; + let word_to_insert = + try + let line_start = get_line_start insert in + let prev_backslash_search = insert#backward_search ~limit:line_start "\\" in + let backslash = + match prev_backslash_search with + | None -> raise Abort + | Some (backslash_start,backslash_stop) -> backslash_start + in + let prefix = backslash#get_text ~stop:insert in + let word = + match lookup prefix with + | None -> + (* show_warning ("No binding match " ^ prefix); *) + raise Abort + | Some word -> word + in + let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in + if not was_deleted then raise Abort; + word + with Abort -> " " + in + let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in + let _was_inserted = buffer#insert_interactive ~iter:insert2 word_to_insert in let () = self#buffer#end_user_action () in self#buffer#delete_mark (`MARK insert_mark) -- cgit v1.2.3 From fbf5696a3b9c90301dd6b8c2eef8f055ba0ff278 Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 26 Sep 2018 11:37:33 +0200 Subject: support for coqide commande line arguments --- ide/coqide.ml | 33 ++++++------ ide/preferences.ml | 139 +++++++++++++++++++++++++++----------------------- ide/preferences.mli | 3 +- ide/wg_ScriptView.ml | 8 ++- ide/wg_ScriptView.mli | 2 +- 5 files changed, 99 insertions(+), 86 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 5e4994eeb8..bc3f5212f6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -766,13 +766,9 @@ let about _ = dialog#set_authors authors; dialog#show () -let latex_to_unicode = +let apply_unicode_binding = cb_on_current_term (fun t -> - (*let show_warning s = - t.messages#clear; - t.messages#add_string s - in*) - t.script#latex_to_unicode() (*show_warning*)) + t.script#apply_unicode_binding()) let comment = cb_on_current_term (fun t -> t.script#comment ()) let uncomment = cb_on_current_term (fun t -> t.script#uncomment ()) @@ -1170,7 +1166,7 @@ let build_ui () = item "Coqtop arguments" ~label:"Coqtop _arguments" ~callback:MiscMenu.coqtop_arguments; item "Latex-to-unicode" ~label:"_Latex-to-unicode" ~accel:"space" - ~callback:MiscMenu.latex_to_unicode; + ~callback:MiscMenu.apply_unicode_binding; ]; menu compile_menu [ @@ -1357,9 +1353,12 @@ let main files = this default coqtop path *) let read_coqide_args argv = - let rec filter_coqtop coqtop project_files out = function + let rec filter_coqtop coqtop project_files bindings_files out = function + |"-unicode-bindings" :: sfilenames :: args -> + let filenames = Str.split (Str.regexp ",") sfilenames in + filter_coqtop coqtop project_files (filenames @ bindings_files) out args |"-coqtop" :: prog :: args -> - if coqtop = None then filter_coqtop (Some prog) project_files out args + if coqtop = None then filter_coqtop (Some prog) project_files bindings_files out args else (output_string stderr "Error: multiple -coqtop options"; exit 1) |"-f" :: file :: args -> if project_files <> None then @@ -1367,7 +1366,7 @@ let read_coqide_args argv = let d = CUnix.canonical_path_name (Filename.dirname file) in let warning_fn x = Format.eprintf "%s@\n%!" x in let p = CoqProject_file.read_project_file ~warning_fn file in - filter_coqtop coqtop (Some (d,p)) out args + filter_coqtop coqtop (Some (d,p)) out bindings_files args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 |"-coqtop" :: [] -> @@ -1376,19 +1375,21 @@ let read_coqide_args argv = Minilib.debug := true; Flags.debug := true; Backtrace.record_backtrace true; - filter_coqtop coqtop project_files ("-debug"::out) args + filter_coqtop coqtop project_files bindings_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; - filter_coqtop coqtop project_files out args + filter_coqtop coqtop project_files bindings_files out args |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg -> (* argument added by MacOS during .app launch *) - filter_coqtop coqtop project_files out args - |arg::args -> filter_coqtop coqtop project_files (arg::out) args - |[] -> (coqtop,project_files,List.rev out) + filter_coqtop coqtop project_files bindings_files out args + |arg::args -> filter_coqtop coqtop project_files bindings_files (arg::out) args + |[] -> (coqtop,project_files,bindings_files,List.rev out) in - let coqtop,project_files,argv = filter_coqtop None None [] argv in + let coqtop,project_files,bindings_files,argv = filter_coqtop None None [] [] argv in + let bindings_files = if bindings_files = [] then ["default"] else bindings_files in Ideutils.custom_coqtop := coqtop; custom_project_file := project_files; + Preferences.load_unicode_bindings_files bindings_files; argv diff --git a/ide/preferences.ml b/ide/preferences.ml index 2701089331..57589b4363 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -29,67 +29,6 @@ type tag = { } -(** Latex to unicode bindings. - - Text description of the unicode bindings, in a file coqide.bindings - one item per line, each item consists of: - - a leading backslahs - - a ascii word next to it - - a unicode word (or possibly a full sentence in-between doube-quotes, - the sentence may include spaces and \n tokens), - - optinally, an integer indicating the "priority" (lower is higher priority), - technically the length of the prefix that suffices to obtain this word. - Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda". - - \pi π - \lambda λ 3 - \lambdas λs 4 - \lake Ο 2 - \lemma "Lemma foo : x. Proof. Qed." 1 - - - In case of equality between two candidates (same ascii word, or same - priorities for two words with similar prefix), the first binding is considered. -*) - -let latex_to_unicode = ref [] - (* dummy default, used for testing - [ - ("\\pi", "π", None); - ("\\lambdas", "λs", Some 4); - ("\\lambda", "λ", Some 3); - ("\\lake", "0", Some 2); - ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); - ] - *) - -let get_latex_to_unicode () = - !latex_to_unicode - -let load_latex_to_unicode_file filename = - let acc = ref [] in - let ch = open_in filename in - begin try while true do - let line = input_line ch in - begin try - let chline = Scanf.Scanning.from_string line in - let (key,value) = - Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in - let prio = - try Scanf.bscanf chline " %d" (fun x -> Some x) - with Scanf.Scan_failure _ | Failure _ | End_of_file -> None - in - acc := (key,value,prio)::!acc; - Scanf.Scanning.close_in chline; - with End_of_file -> () end; - done with End_of_file -> () end; - close_in ch; - latex_to_unicode := List.rev !acc - (*List.iter (fun (x,y,p) -> - Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) - !latex_to_unicode; - prerr_newline() *) - - (** Generic preferences *) type obj = { @@ -310,7 +249,7 @@ let loaded_accel_file = try get_config_file "coqide.keys" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" -let loaded_bindings_file = +let loaded_default_unicode_bindings_file = try get_config_file "coqide.bindings" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings" @@ -709,7 +648,6 @@ let save_pref () = let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - let () = load_latex_to_unicode_file loaded_bindings_file in let m = Config_lexer.load_file loaded_pref_file in let iter name v = @@ -1073,3 +1011,78 @@ let configure ?(apply=(fun () -> ())) parent = match x with | Return_apply | Return_ok -> save_pref () | Return_cancel -> () + +(********************************************************************) + +(** Latex to unicode bindings. + + Text description of the unicode bindings, in a file coqide.bindings + one item per line, each item consists of: + - a leading backslahs + - a ascii word next to it + - a unicode word (or possibly a full sentence in-between doube-quotes, + the sentence may include spaces and \n tokens), + - optinally, an integer indicating the "priority" (lower is higher priority), + technically the length of the prefix that suffices to obtain this word. + Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda". + + \pi π + \lambda λ 3 + \lambdas λs 4 + \lake Ο 2 + \lemma "Lemma foo : x. Proof. Qed." 1 ---currently not supported by parser + + - In case of equality between two candidates (same ascii word, or same + priorities for two words with similar prefix), the first binding is considered. + + - Note that if a same token is bound in several bindings file, + the one with the lowest priority number will be considered. + In case of same priority, the binding from the first loaded file is considered. +*) + +let unicode_bindings = ref [] + (* example unicode bindings table: + [ ("\\pi", "π", None); + ("\\lambdas", "λs", Some 4); + ("\\lambda", "λ", Some 3); + ("\\lake", "0", Some 2); + ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] *) + +let get_unicode_bindings () = + !unicode_bindings + +let process_unicode_bindings_file filename = + if not (Sys.file_exists filename) then begin + output_string stderr (Printf.sprintf "Error: unicode bindings file '%s' was not found.\n" filename); exit 1 + end; + let ch = open_in filename in + begin try while true do + let line = input_line ch in + begin try + let chline = Scanf.Scanning.from_string line in + let (key,value) = + Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in + let prio = + try Scanf.bscanf chline " %d" (fun x -> Some x) + with Scanf.Scan_failure _ | Failure _ | End_of_file -> None + in + unicode_bindings := (key,value,prio)::!unicode_bindings; + (* Note: storing bindings in reverse order, flipping is done later *) + Scanf.Scanning.close_in chline; + with End_of_file -> () end; + done with End_of_file -> () end; + close_in ch + +let load_unicode_bindings_files filenames = + let filenames = List.map (fun f -> + if f = "default" then loaded_default_unicode_bindings_file else f) filenames in + List.iter process_unicode_bindings_file filenames; + unicode_bindings := List.rev !unicode_bindings + + (* For debugging unicode bindings: + let print_unicode_bindings () = + List.iter (fun (x,y,p) -> + Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) + !unicode_bindings; + prerr_newline() + *) diff --git a/ide/preferences.mli b/ide/preferences.mli index 52303ea6cf..a75f1b3cec 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -112,4 +112,5 @@ val stick : 'a preference -> val use_default_doc_url : string -val get_latex_to_unicode : unit -> (string * string * int option) list +val get_unicode_bindings : unit -> (string * string * int option) list +val load_unicode_bindings_files : string list -> unit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 97bf9aefc5..efacaee577 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -407,8 +407,8 @@ object (self) self#buffer#delete_mark (`MARK stop_mark) | _ -> () - method latex_to_unicode () (* (show_warning:string->unit) *) = - let bindings = Preferences.get_latex_to_unicode() in + method apply_unicode_binding () = + let bindings = Preferences.get_unicode_bindings() in (** Auxiliary function to test whether [s] is a prefix of [str]; Note that there might be overlap with wg_Completion::is_substring *) let string_is_prefix s str = @@ -459,9 +459,7 @@ object (self) let prefix = backslash#get_text ~stop:insert in let word = match lookup prefix with - | None -> - (* show_warning ("No binding match " ^ prefix); *) - raise Abort + | None -> raise Abort | Some word -> word in let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index eb1beedfad..ca35b7fb67 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -26,7 +26,7 @@ object method set_show_right_margin : bool -> unit method comment : unit -> unit method uncomment : unit -> unit - method latex_to_unicode : unit -> unit (* (string -> unit) -> unit *) + method apply_unicode_binding : unit -> unit (* (string -> unit) -> unit *) method recenter_insert : unit method complete_popup : Wg_Completion.complete_popup end -- cgit v1.2.3 From 9883bde37482632e135895d75fae973ef8b89a08 Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 26 Sep 2018 15:30:21 +0200 Subject: cosmetic changes --- ide/wg_ScriptView.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index ca35b7fb67..df475f0e66 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -26,7 +26,7 @@ object method set_show_right_margin : bool -> unit method comment : unit -> unit method uncomment : unit -> unit - method apply_unicode_binding : unit -> unit (* (string -> unit) -> unit *) + method apply_unicode_binding : unit -> unit method recenter_insert : unit method complete_popup : Wg_Completion.complete_popup end -- cgit v1.2.3 From 7b0b7e8440829f80d1fdee1a7f6daa82d3538c90 Mon Sep 17 00:00:00 2001 From: charguer Date: Mon, 12 Nov 2018 16:28:14 +0100 Subject: binding generator for coqide --- Makefile | 1 + Makefile.ide | 17 +- ide/default.bindings | 1156 ----------------- ide/default_bindings_src.ml | 2899 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 2915 insertions(+), 1158 deletions(-) delete mode 100644 ide/default.bindings create mode 100644 ide/default_bindings_src.ml diff --git a/Makefile b/Makefile index 6adefa5d47..2b5d2cea16 100644 --- a/Makefile +++ b/Makefile @@ -263,6 +263,7 @@ clean-ide: rm -f ide/input_method_lexer.ml rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml + rm -f ide/default.bindings rm -rf $(COQIDEAPP) mlgclean: diff --git a/Makefile.ide b/Makefile.ide index db1cc3746d..f26c9bd282 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -52,7 +52,11 @@ IDETOPBYTE=bin/coqidetop.byte$(EXE) LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml -IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map +IDEBINDINGS:=ide/default.bindings +IDEBINDINGSSRC:=ide/default_bindings_src.ml +IDEBINDINGSEXE:=ide/default_bindings_src.exe + +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map $(IDEBINDINGS) ## GTK for Coqide MacOS bundle @@ -66,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share # CoqIde special targets ########################################################################### -.PHONY: coqide coqide-opt coqide-byte coqide-files coqide-binaries +.PHONY: coqide coqide-opt coqide-byte coqide-bindings coqide-files coqide-binaries .PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde (native version) and the stuff needed to lauch it @@ -159,6 +163,15 @@ $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SYSMOD) \ $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@ +coqide-bindings: $(IDEBINDINGS) + +$(IDEBINDINGSEXE): $(IDEBINDINGSSRC) + $(OCAMLC) $< -o $@ + +$(IDEBINDINGS): $(IDEBINDINGSEXE) + $< $@ + + #################### ## Install targets #################### diff --git a/ide/default.bindings b/ide/default.bindings deleted file mode 100644 index ac4d32fb34..0000000000 --- a/ide/default.bindings +++ /dev/null @@ -1,1156 +0,0 @@ -\!' ¡ -\` ‘ -\`` “ -\' ′ -\'' ″ -\''' ‴ -\mbox'' ” -\mbox' ’ -\-- – -\--- — -\"A Ä -\"E Ë -\"H Ḧ -\"I Ï -\"O Ö -\"U Ü -\"W Ẅ -\"X Ẍ -\"Y Ÿ -\"a ä -\"e ë -\"h ḧ -\"i ï -\"o ö -\"t ẗ -\"u ü -\"w ẅ -\"x ẍ -\"y ÿ -\'A Á -\'C Ć -\'E É -\'G Ǵ -\'I Í -\'K Ḱ -\'L Ĺ -\'M Ḿ -\'N Ń -\'O Ó -\'P Ṕ -\'R Ŕ -\'S Ś -\'U Ú -\'W Ẃ -\'Y Ý -\'Z Ź -\'a á -\'c ć -\'e é -\'g ǵ -\'i í -\'k ḱ -\'l ĺ -\'m ḿ -\'n ń -\'o ó -\'p ṕ -\'r ŕ -\'s ś -\'u ú -\'w ẃ -\'y ý -\'z ź -\.A Ȧ -\.B Ḃ -\.C Ċ -\.D Ḋ -\.E Ė -\.F Ḟ -\.G Ġ -\.H Ḣ -\.I İ -\.M Ṁ -\.N Ṅ -\.O Ȯ -\.P Ṗ -\.R Ṙ -\.S Ṡ -\.T Ṫ -\.W Ẇ -\.X Ẋ -\.Y Ẏ -\.Z Ż -\.a ȧ -\.b ḃ -\.c ċ -\.d ḋ -\.e ė -\.f ḟ -\.g ġ -\.h ḣ -\.m ṁ -\.n ṅ -\.o ȯ -\.p ṗ -\.r ṙ -\.s ṡ -\.t ṫ -\.w ẇ -\.x ẋ -\.y ẏ -\.z ż -\=A Ā -\=E Ē -\=G Ḡ -\=I Ī -\=O Ō -\=U Ū -\=Y Ȳ -\=a ā -\=e ē -\=g ḡ -\=i ī -\=o ō -\=u ū -\=y ȳ -\AA Å -\AE Æ -\Alpha Α 1 -\Beta Β 1 -\Box □ -\Bumpeq ≎ -\Cap ⋒ -\Chi Χ 1 -\Cup ⋓ -\DH Ð -\Delta Δ 1 -\Diamond ◇ -\Downarrow ⇓ -\Epsilon Ε 1 -\Eta Η 1 -\Finv Ⅎ -\Gamma Γ 1 -\Im ℑ -\Join ⋈ -\Kappa Κ 1 -\L Ł -\Lambda Λ 1 -\Leftarrow ⇐ -\Leftrightarrow ⇔ -\Lleftarrow ⇚ -\Longleftarrow ⇐ -\Longleftrightarrow ⇔ -\Longrightarrow ⇒ -\Lsh ↰ -\Mu Μ 1 -\Nu Ν 1 -\O Ø -\OE Œ -\Omega Ω -\W Ω 1 -\Omicron Ο 1 -\P ¶ -\Phi Φ -\F Φ 1 -\Pi Π 1 -\Psi Ψ -\Re ℜ -\Rho Ρ 1 -\Rightarrow ⇒ -\Rrightarrow ⇛ -\Rsh ↱ -\S § -\Sigma Σ 1 -\Subset ⋐ -\Supset ⋑ -\TH Þ -\Tau Τ 1 -\Theta Θ 1 -\Uparrow ⇑ -\Updownarrow ⇕ -\Upsilon Υ 1 -\Vdash ⊩ -\Vvdash ⊪ -\Xi Ξ 1 -\Zeta Ζ 1 -\^A  -\^C Ĉ -\^E Ê -\^G Ĝ -\^H Ĥ -\^I Î -\^J Ĵ -\^O Ô -\^S Ŝ -\^U Û -\^W Ŵ -\^Y Ŷ -\^Z Ẑ -\^a â -\^c ĉ -\^e ê -\^g ĝ -\^h ĥ -\^i î -\^j ĵ -\^o ô -\^s ŝ -\^u û -\^w ŵ -\^y ŷ -\^z ẑ -\`A À -\`E È -\`I Ì -\`N Ǹ -\`O Ò -\`U Ù -\`W Ẁ -\`Y Ỳ -\`a à -\`e è -\`i ì -\`n ǹ -\`o ò -\`u ù -\`w ẁ -\`y ỳ -\aa å -\ae æ -\aleph ℵ -\alpha α 1 -\angle ∠ -\approx ≈ -\approxeq ≊ -\aquarius ♒ -\aries ♈ -\ascnode ☊ -\ast ∗ -\astrosun ☉ -\asymp ≍ -\backepsilon ∍ -\backprime ‵ -\backsim ∽ -\barwedge ⊼ -\barA Ā -\barE Ē -\barG Ḡ -\barI Ī -\barO Ō -\barU Ū -\barY Ȳ -\bara ā -\bare ē -\barg ḡ -\bari ī -\baro ō -\baru ū -\bary ȳ -\because ∵ -\beta β 1 -\beth ℶ -\between ≬ -\bigcap ⋂ -\bigcirc ○ -\bigcup ⋃ -\bigodot ⊙ -\bigoplus ⊕ -\bigotimes ⊗ -\bigsqcup ⊔ -\bigstar ★ -\bigtriangledown ▽ -\bigtriangleup △ -\biguplus ⊎ -\bigvee ⋁ -\bigwedge ⋀ -\blackbishop ♝ -\blackking ♚ -\blackknight ♞ -\blacklozenge ◆ -\blackpawn ♟ -\blackqueen ♛ -\blackrook ♜ -\blacksquare ■ -\blacktriangle ▲ -\blacktriangledown ▼ -\blacktriangleleft ◀ -\blacktriangleright ▷ -\bot ⊥ -\bowtie ⋈ -\boxdot ⊡ -\boxminus ⊟ -\boxplus ⊞ -\boxtimes ⊠ -\breveA Ă -\breveE Ĕ -\breveG Ğ -\breveI Ĭ -\breveO Ŏ -\breveU Ŭ -\brevea ă -\brevee ĕ -\breveg ğ -\brevei ĭ -\breveo ŏ -\breveu ŭ -\bullet ∙ -\bumpeq ≏ -\cancer ♋ -\cap ∩ -\capricornus ♑ -\capslockkey ⇪ -\cdot ⋅ -\cdots ⋯ -\centerdot ⋅ -\cents ¢ -\checkA Ǎ -\checkC Č -\checkD Ď -\checkE Ě -\checkN Ň -\checkR Ř -\checkS Š -\checkT Ť -\checkZ Ž -\checka ǎ -\checkc č -\checkd ď -\checke ě -\checkn ň -\checkr ř -\checks š -\checkt ť -\checkz ž -\chi χ 1 -\circ ∘ -\circeq ≗ -\circlearrowleft ↺ -\circlearrowright ↻ -\circledS Ⓢ -\circledast ⊛ -\circledcirc ⊚ -\circleddash ⊝ -\clubsuit ♣ -\cmdkey ⌘ -\complement ∁ -\cong ≅ -\conjunction ☌ -\coprod ∐ -\copyright © -\cup ∪ -\curlyeqprec ⋞ -\curlyeqsucc ⋟ -\curlyvee ⋎ -\curlywedge ⋏ -\curvearrowleft ↶ -\curvearrowright ↷ -\cC Ç -\cc ç -\dag † -\dagger † -\daleth ℸ -\dashleftarrow ⇠ -\dashrightarrow ⇢ -\dashv ⊣ -\ddag ‡ -\ddagger ‡ -\ddots ⋱ -\ddotA Ä -\ddotE Ë -\ddotH Ḧ -\ddotI Ï -\ddotO Ö -\ddotU Ü -\ddotW Ẅ -\ddotX Ẍ -\ddotY Ÿ -\ddota ä -\ddote ë -\ddoth ḧ -\ddoti ï -\ddoto ö -\ddott ẗ -\ddotu ü -\ddotw ẅ -\ddotx ẍ -\ddoty ÿ -\degree ° -\delkey ⌫ -\delta δ 1 -\descnode ☋ -\dh ð -\diamond ⋄ -\diamondsuit ♢ -\digamma Ϝ -\div ÷ -\divideontimes ⋇ -\doteq ≐ -\doteqdot ≑ -\dotplus ∔ -\dotA Ȧ -\dotB Ḃ -\dotC Ċ -\dotD Ḋ -\dotE Ė -\dotF Ḟ -\dotG Ġ -\dotH Ḣ -\dotI İ -\dotM Ṁ -\dotN Ṅ -\dotO Ȯ -\dotP Ṗ -\dotR Ṙ -\dotS Ṡ -\dotT Ṫ -\dotW Ẇ -\dotX Ẋ -\dotY Ẏ -\dotZ Ż -\dota ȧ -\dotb ḃ -\dotc ċ -\dotd ḋ -\dote ė -\dotf ḟ -\dotg ġ -\doth ḣ -\dotm ṁ -\dotn ṅ -\doto ȯ -\dotp ṗ -\dotr ṙ -\dots ṡ -\dott ṫ -\dotw ẇ -\dotx ẋ -\doty ẏ -\dotz ż -\downarrow ↓ -\downdownarrows ⇊ -\downharpoonleft ⇃ -\downharpoonright ⇂ -\dA Ạ -\dB Ḅ -\dD Ḍ -\dE Ẹ -\dH Ḥ -\dI Ị -\dK Ḳ -\dL Ḷ -\dM Ṃ -\dN Ṇ -\dO Ọ -\dR Ṛ -\dS Ṣ -\dT Ṭ -\dU Ụ -\dV Ṿ -\dW Ẉ -\dY Ỵ -\dZ Ẓ -\da ạ -\db ḅ -\dd ḍ -\de ẹ -\dh ḥ -\di ị -\dk ḳ -\dl ḷ -\dm ṃ -\dn ṇ -\do ọ -\dr ṛ -\ds ṣ -\dt ṭ -\du ụ -\dv ṿ -\dw ẉ -\dy ỵ -\dz ẓ -\earth ⊕ -\ejectkey ⏏ -\ell ℓ -\emptyset ∅ -\enterkey ⌤ -\epsdice1 ⚀ -\epsdice2 ⚁ -\epsdice3 ⚂ -\epsdice4 ⚃ -\epsdice5 ⚄ -\epsdice6 ⚅ -\epsilon ∊ -\eqcirc ≖ -\equiv ≡ -\esckey ⎋ -\eta η 1 -\eth ð -\euro € -\exists ∃ -\fallingdotseq ≒ -\flat ♭ -\forall ∀ -\frown ⌢ -\gamma γ 1 -\ge ≥ -\gemini ♊ -\geq ≥ -\geqq ≧ -\gg ≫ -\ggg ⋙ -\gimel ℷ -\gtrdot ⋗ -\gtreqless ⋛ -\gtrless ≷ -\gtrsim ≳ -\hbar ℏ -\heartsuit ♡ -\hookleftarrow ↩ -\hookrightarrow ↪ -\hslash ℏ -\iiiint ⨌ -\iiint ∭ -\iint ∬ -\implies ⇒ -\in ∈ -\infty ∞ -\int ∫ -\intercal ⊺ -\iota ι 1 -\jupiter ♃ -\kappa κ 1 -\l{} ł -\lambda λ 1 -\langle ⟨ -\lceil ⌈ -\ldots … -\le ≤ -\leadsto ↝ -\leftarrow ← -\leftarrowtail ↢ -\leftharpoondown ↽ -\leftharpoonup ↼ -\leftleftarrows ⇇ -\leftmoon ☾ -\leftrightarrow ↔ -\leftrightarrows ⇆ -\leftrightharpoons ⇋ -\leftrightsquigarrow ↭ -\leftthreetimes ⋋ -\leo ♌ -\leq ≤ -\leqq ≦ -\leqslant ≤ -\lessdot ⋖ -\lesseqgtr ⋚ -\lessgtr ≶ -\lesssim ≲ -\lfloor ⌊ -\lhd ⊲ -\libra ♎ -\ll ≪ -\lll ⋘ -\longleftarrow ← -\longleftrightarrow ↔ -\longmapsto ⇖ -\longrightarrow → -\looparrowleft ↫ -\looparrowright ↬ -\lozenge ◊ -\ltimes ⋉ -\mapsto ↦ -\mars ♂ -\bb0 𝟘 -\bb1 𝟙 -\bb2 𝟚 -\bb3 𝟛 -\bb4 𝟜 -\bb5 𝟝 -\bb6 𝟞 -\bb7 𝟟 -\bb8 𝟠 -\bb9 𝟡 -\bbA 𝔸 -\bbB 𝔹 -\bbC ℂ -\bbD 𝔻 -\bbE 𝔼 -\bbF 𝔽 -\bbG 𝔾 -\bbH ℍ -\bbI 𝕀 -\bbJ 𝕁 -\bbK 𝕂 -\bbL 𝕃 -\bbM 𝕄 -\bbN ℕ -\bbO 𝕆 -\bbP ℙ -\bbQ ℚ -\bbR ℝ -\bbS 𝕊 -\bbT 𝕋 -\bbU 𝕌 -\bbV 𝕍 -\bbW 𝕎 -\bbX 𝕏 -\bbY 𝕐 -\bbZ ℤ -\bba 𝕒 -\bbb 𝕓 -\bbc 𝕔 -\bbd 𝕕 -\bbe 𝕖 -\bbf 𝕗 -\bbg 𝕘 -\bbh 𝕙 -\bbi 𝕚 -\bbj 𝕛 -\bbk 𝕜 -\bbl 𝕝 -\bbm 𝕞 -\bbn 𝕟 -\bbo 𝕠 -\bbp 𝕡 -\bbq 𝕢 -\bbr 𝕣 -\bbs 𝕤 -\bbt 𝕥 -\bbu 𝕦 -\bbv 𝕧 -\bbw 𝕨 -\bbx 𝕩 -\bby 𝕪 -\bbz 𝕫 -\calA 𝒜 -\calB ℬ -\calC 𝒞 -\calD 𝒟 -\calE ℰ -\calF ℱ -\calG 𝒢 -\calH ℋ -\calI ℐ -\calJ 𝒥 -\calK 𝒦 -\calL ℒ -\calM ℳ -\calN 𝒩 -\calO 𝒪 -\calP 𝒫 -\calQ 𝒬 -\calR ℛ -\calS 𝒮 -\calT 𝒯 -\calU 𝒰 -\calV 𝒱 -\calW 𝒲 -\calX 𝒳 -\calY 𝒴 -\calZ 𝒵 -\cala 𝒶 -\calb 𝒷 -\calc 𝒸 -\cald 𝒹 -\cale ℯ -\calf 𝒻 -\calg ℊ -\calh 𝒽 -\cali 𝒾 -\calj 𝒿 -\calk 𝓀 -\call 𝓁 -\calm 𝓂 -\caln 𝓃 -\calo ℴ -\calp 𝓅 -\calq 𝓆 -\calr 𝓇 -\cals 𝓈 -\calt 𝓉 -\calu 𝓊 -\calv 𝓋 -\calw 𝓌 -\calx 𝓍 -\caly 𝓎 -\calz 𝓏 -\frakA 𝔄 -\frakB 𝔅 -\frakC ℭ -\frakD 𝔇 -\frakE 𝔈 -\frakF 𝔉 -\frakG 𝔊 -\frakH ℌ -\frakI ℑ -\frakJ 𝔍 -\frakK 𝔎 -\frakL 𝔏 -\frakM 𝔐 -\frakN 𝔑 -\frakO 𝔒 -\frakP 𝔓 -\frakQ 𝔔 -\frakR ℜ -\frakS 𝔖 -\frakT 𝔗 -\frakU 𝔘 -\frakV 𝔙 -\frakW 𝔚 -\frakX 𝔛 -\frakY 𝔜 -\frakZ ℨ -\fraka 𝔞 -\frakb 𝔟 -\frakc 𝔠 -\frakd 𝔡 -\frake 𝔢 -\frakf 𝔣 -\frakg 𝔤 -\frakh 𝔥 -\fraki 𝔦 -\frakj 𝔧 -\frakk 𝔨 -\frakl 𝔩 -\frakm 𝔪 -\frakn 𝔫 -\frako 𝔬 -\frakp 𝔭 -\frakq 𝔮 -\frakr 𝔯 -\fraks 𝔰 -\frakt 𝔱 -\fraku 𝔲 -\frakv 𝔳 -\frakw 𝔴 -\frakx 𝔵 -\fraky 𝔶 -\frakz 𝔷 -\measuredangle ∡ -\mercury ☿ -\mho ℧ -\mid ∣ -\models ⊨ -\mp ∓ -\mu μ 1 -\multimap ⊸ -\nabla ∇ -\natural ♮ -\nearrow ↗ -\neg ¬ -\neptune ♆ -\neq ≠ -\nexists ∄ -\ng ŋ -\ni ∋ -\not< ≮ -\not> ≯ -\not\Vdash ⊮ -\not\approx ≉ -\not\cong ≇ -\not\equiv ≢ -\not\ge ≱ -\not\gtrless ≹ -\not\in ∉ -\not\le ≰ -\not\models ⊭ -\not\ni ∌ -\not\sim ≄ -\not\sqsubseteq ⋢ -\not\sqsupseteq ⋣ -\not\subset ⊄ -\not\subseteq ⊈ -\not\supset ⊅ -\not\supseteq ⊉ -\not\vdash ⊬ -\notin ∉ -\nu ν 1 -\v ν 1 -\nwarrow ↖ -\o{} ø -\odot ⊙ -\oe œ -\oint ∮ -\omega ω -\w ω 1 -\omicron ο 1 -\ominus ⊖ -\oplus ⊕ -\opposition ☍ -\optkey ⌥ -\oslash ⊘ -\otimes ⊗ -\parallel ∥ -\partial ∂ -\perp ⊥ -\phi φ -\f φ 1 -\pi π 1 -\pilcrow ¶ -\pisces ♓ -\pitchfork ⋔ -\pluto ♇ -\pm ± -\pound £ -\pounds £ -\prec ≺ -\preccurlyeq ≼ -\preceq ≼ -\precsim ≾ -\prime ′ -\prod ∏ -\propto ∝ -\psi ψ -\rangle ⟩ -\rceil ⌉ -\registered ® -\returnkey ⏎ -\revtabkey ⇤ -\rfloor ⌋ -\rhd ⊳ -\rho ρ 1 -\rightarrow → -\rightarrowtail ↣ -\rightdelkey ⌦ -\rightharpoondown ⇁ -\rightharpoonup ⇀ -\rightleftarrows ⇄ -\rightleftharpoons ⇌ -\rightmoon ☽ -\rightrightarrows ⇉ -\rightsquigarrow ⇝ -\rightthreetimes ⋌ -\risingdotseq ≓ -\rtimes ⋊ -\sagittarius ♐ -\saturn ♄ -\scorpio ♏ -\searrow ↘ -\section § -\setminus ∖ -\sharp ♯ -\shiftkey ⇧ -\shortparallel ∥ -\sigma σ 1 -\sim ∼ -\simeq ≃ -\smallfrown ⌢ -\smallsetminus ∖ -\smallsmile ⌣ -\smile ⌣ -\space ␣ -\spadesuit ♠ -\sphericalangle ∢ -\sqcap ⊓ -\sqcup ⊔ -\sqsubset ⊏ -\sqsubseteq ⊑ -\sqsupset ⊐ -\sqsupseteq ⊒ -\square □ -\ss ß -\star ⋆ -\subset ⊂ -\subseteq ⊆ -\subsetneq ⊊ -\succ ≻ -\succcurlyeq ≽ -\succeq ≽ -\succsim ≿ -\sum ∑ -\supset ⊃ -\supseteq ⊇ -\supsetneq ⊋ -\surd √ -\swarrow ↙ -\tabkey ⇥ -\tau τ 1 -\taurus ♉ -\textbabygamma ɤ -\textbarglotstop ʡ -\textbari ɨ -\textbaro ɵ -\textbarrevglotstop ʢ -\textbaru ʉ -\textbeltl ɬ -\textbeta β -\textbullseye ʘ -\textchi χ -\textcloserevepsilon ɞ -\textcrh ħ -\textctc ɕ -\textctj ʝ -\textctz ʑ -\textdoublepipe ǁ -\textdyoghlig ʤ -\textepsilon ɛ -\textesh ʃ -\textfishhookr ɾ -\textgamma ɣ -\textglotstop ʔ -\textgrgamma γ -\texthtb ɓ -\texthtd ɗ -\texthtg ɠ -\texthth ɦ -\texththeng ɧ -\texthtscg ʛ -\textinvscr ʁ -\textiota ι -\textltailm ɱ -\textltailn ɲ -\textltilde ɫ -\textlyoghlig ɮ -\textopeno ɔ -\textphi ɸ -\textpipe ǀ -\textregistered ® -\textreve ɘ -\textrevepsilon ɜ -\textrevglotstop ʕ -\textrhookrevepsilon ɝ -\textrighthookschwa ɚ -\textrtaild ɖ -\textrtaill ɭ -\textrtailn ɳ -\textrtailr ɽ -\textrtails ʂ -\textrtailt ʈ -\textrtailz ʐ -\textscb ʙ -\textscg ɢ -\textsch ʜ -\textschwa ə -\textsci ɪ -\textscl ʟ -\textscn ɴ -\textscoelig ɶ -\textscr ʀ -\textscripta ɑ -\textscriptv ʋ -\textscy ʏ -\textteshlig ʧ -\texttheta θ -\texttrademark ™ -\textturna ɐ -\textturnh ɥ -\textturnlonglegr ɺ -\textturnm ɯ -\textturnmrleg ɰ -\textturnr ɹ -\textturnrrtail ɻ -\textturnscripta ɒ -\textturnv ʌ -\textturnw ʍ -\textturny ʎ -\textupsilon ʊ -\textyogh ʒ -\th þ -\therefore ∴ -\theta θ 1 -\h θ 1 -\thickapprox ≈ -\thicksim ∼ -\times × -\top ⊤ -\trademark ™ -\triangle △ -\triangledown ▽ -\triangleleft ◁ -\trianglelefteq ⊴ -\triangleq ≜ -\triangleright ▷ -\trianglerighteq ⊵ -\twoheadleftarrow ↞ -\twoheadrightarrow ↠ -\unlhd ⊴ -\unrhd ⊵ -\uparrow ↑ -\updownarrow ↕ -\upharpoonleft ↿ -\upharpoonright ↾ -\uplus ⊎ -\upsilon υ 1 -\upuparrows ⇈ -\uranus ⛢ -\uA Ă -\uE Ĕ -\uG Ğ -\uI Ĭ -\uO Ŏ -\uU Ŭ -\ua ă -\ue ĕ -\ug ğ -\ui ĭ -\uo ŏ -\uu ŭ -\vDash ⊨ -\varepsilon ε -\varkappa ϰ -\varnothing ∅ -\varphi ϕ -\varpi ϖ -\varpropto ∝ -\varrho ϱ -\varsigma ς -\vartheta ϑ -\vartriangle △ -\vartriangleleft ⊲ -\vartriangleright ⊳ -\vdash ⊢ -\vdots ⋮ -\vee ∨ -\veebar ⊻ -\venus ♀ -\virgo ♍ -\vA Ǎ -\vC Č -\vD Ď -\vE Ě -\vN Ň -\vR Ř -\vS Š -\vT Ť -\vZ Ž -\va ǎ -\vc č -\vd ď -\ve ě -\vn ň -\vr ř -\vs š -\vt ť -\vz ž -\wedge ∧ -\whitebishop ♗ -\whiteking ♔ -\whiteknight ♘ -\whitepawn ♙ -\whitequeen ♕ -\whiterook ♖ -\wp ℘ -\wr ≀ -\xi ξ -\zeta ζ 1 -\~A Ā -\~E Ẽ -\~I Ĩ -\~N Ñ -\~O Õ -\~U Ũ -\~Y Ỹ -\~a ã -\~e ẽ -\~i ĩ -\~n ñ -\~o õ -\~u ũ -\~y ỹ -\^( ⁽ -\^) ⁾ -\^+ ⁺ -\^- ⁻ -\^0 ⁰ -\^1 ¹ -\^2 ² -\^3 ³ -\^4 ⁴ -\^5 ⁵ -\^6 ⁶ -\^7 ⁷ -\^8 ⁸ -\^9 ⁹ -\^= ⁼ -\^A ᴬ -\^B ᴮ -\^D ᴰ -\^E ᴱ -\^G ᴳ -\^H ᴴ -\^I ᴵ -\^J ᴶ -\^K ᴷ -\^L ᴸ -\^M ᴹ -\^N ᴺ -\^O ᴼ -\^P ᴾ -\^R ᴿ -\^T ᵀ -\^U ᵁ -\^V ⱽ -\^W ᵂ -\^alpha ᵅ -\^beta ᵝ -\^chi ᵡ -\^delta ᵟ -\^epsilon ᵋ -\^gamma ᵞ -\^iota ᶥ -\^phi ᶲ -\^theta ᶿ -\^varphi ᵠ -\^a ᵃ -\^b ᵇ -\^c ᶜ -\^d ᵈ -\^e ᵉ -\^f ᶠ -\^g ᵍ -\^h ʰ -\^i ⁱ -\^j ʲ -\^k ᵏ -\^l ˡ -\^m ᵐ -\^n ⁿ -\^o ᵒ -\^p ᵖ -\^r ʳ -\^s ˢ -\^t ᵗ -\^u ᵘ -\^v ᵛ -\^w ʷ -\^x ˣ -\^y ʸ -\^z ᶻ -\_( ₍ -\_) ₎ -\_+ ₊ -\_- ₋ -\_0 ₀ -\_1 ₁ -\_2 ₂ -\_3 ₃ -\_4 ₄ -\_5 ₅ -\_6 ₆ -\_7 ₇ -\_8 ₈ -\_9 ₉ -\_= ₌ -\_beta ᵦ -\_chi ᵪ -\_gamma ᵧ -\_rho ᵨ -\_varphi ᵩ -\_a ₐ -\_e ₑ -\_h ₕ -\_i ᵢ -\_j ⱼ -\_k ₖ -\_l ₗ -\_m ₘ -\_n ₙ -\_o ₒ -\_p ₚ -\_r ᵣ -\_s ₛ -\_t ₜ -\_u ᵤ -\_v ᵥ -\_x ₓ diff --git a/ide/default_bindings_src.ml b/ide/default_bindings_src.ml new file mode 100644 index 0000000000..8d2291fcf9 --- /dev/null +++ b/ide/default_bindings_src.ml @@ -0,0 +1,2899 @@ +(** Usage + ocamlc default_bindings_src.ml -o generator.out + ./generator.out output_filename +*) + +(** **************************************************************************) +(** * Classifiers *) + +(** Note: for future use *) + +let logic = "logic" +let symbol = "symbols" +let fraction = "fractions" +let letter = "letters" +let greek_letter = "greek letter" +let asciiart = "ASCII art" +let equivalence = "equivalence relations" +let order = "order relations" +let circle = "circles" +let square = "squares" +let triangle = "triangles" +let arrow = "arrows" +let set = "set theory" +let math = "mathematics" +let space = "spaces" +let delimiter = "parentheses and delimiters" +let miscellanea = "miscellanea" + + +(** **************************************************************************) +(** * Bindings set 1 *) + +let bindings_set_1 = [ + +(* {{{ logics *) + ["\\not"; "\\neg"; "\\lnot" ], "¬", [logic]; + ["\\ForAll"; "\\forall" ], "∀", [logic]; + ["\\exist"; "\\Exists"; "\\exists" ], "∃", [logic]; + ["\\nexist"; "\\nexists"; "\\NotExists" ], "∄", [logic]; + ["\\and"; "\\land"; "\\wedge" ], "∧", [logic]; + ["\\or"; "\\vee"; "\\lor" ], "∨", [logic]; + ["\\vdash"; "\\RightTee" ], "⊢", [logic]; + ["\\dashv"; "\\LeftTee" ], "⊣", [logic]; + ["\\top"; "\\DownTee" ], "⊤", [logic]; + ["\\bot"; "\\perp"; "\\UpTee"; "\\bottom" ], "⊥", [logic]; + ["\\models" ], "⊧", [logic]; + ["\\vDash"; "\\DoubleRightTee" ], "⊨", [logic]; + ["\\Vdash" ], "⊩", [logic]; + ["\\Vvdash" ], "⊪", [logic]; + ["\\VDash" ], "⊫", [logic]; + ["\\nvdash" ], "⊬", [logic]; + ["\\nvDash" ], "⊭", [logic]; + ["\\nVdash" ], "⊮", [logic]; + ["\\nVDash" ], "⊯", [logic]; + ["\\Wedge"; "\\xwedge"; "\\bigwedge" ], "⋀", [logic]; + ["\\Vee"; "\\xvee"; "\\bigvee" ], "⋁", [logic]; +(* }}} *) + +(* {{{ symbols *) + ["\\cent" ], "¢", [symbol]; + ["\\pound" ], "£", [symbol]; + ["\\curren" ], "¤", [symbol]; + ["\\yen" ], "¥", [symbol]; + ["\\brvbar" ], "¦", [symbol]; + ["\\sect" ], "§", [symbol]; + ["\\uml"; "\\die"; "\\Dot"; "\\DoubleDot" ], "¨", [symbol]; + ["\\macr"; "\\OverBar" ], "¯", [symbol]; + ["\\sup" ], "^", [symbol]; + ["\\sup2" ], "²", [symbol]; + ["\\sup3" ], "³", [symbol]; + ["\\acute"; "\\DiacriticalAcute" ], "´", [symbol]; + ["\\para" ], "¶", [symbol]; + ["\\middot"; "\\centerdot"; "\\CenterDot" ], "·", [symbol]; + ["\\cedil"; "\\Cedilla" ], "¸", [symbol]; + ["\\sup1" ], "¹", [symbol]; + ["\\iquest" ], "¿", [symbol]; + ["\\thorn" ], "þ", [symbol]; + ["\\imath"; "\\inodot" ], "ı", [symbol]; + ["\\Hacek"; "\\caron" ], "ˇ", [symbol]; + ["\\Breve"; "\\breve" ], "˘", [symbol]; + ["\\dot"; "\\DiacriticalDot" ], "˙", [symbol]; + ["\\ogon" ], "˛", [symbol]; + ["\\tilde"; "\\DiacriticalTilde" ], "˜", [symbol]; + ["\\dblac"; "\\DiacriticalDoubleAcute" ], "˝", [symbol]; + ["\\Hat" ], "̂", [symbol]; + ["\\DownBreve" ], "̑", [symbol]; + ["\\UnderBar" ], "̲", [symbol]; + ["\\dash"; "\\hyphen" ], "‐", [symbol]; + ["\\ndash" ], "–", [symbol]; + ["\\mdash" ], "—", [symbol]; + ["\\horbar" ], "―", [symbol]; + ["\\Vert"; "\\Verbar" ], "‖", [symbol]; + ["\\lsquo"; "\\OpenCurlyQuote" ], "‘", [symbol]; + ["\\rsquo"; "\\rsquor"; "\\CloseCurlyQuote" ], "’", [symbol]; + ["\\lsquor" ], "‚", [symbol]; + ["\\ldquo"; "\\OpenCurlyDoubleQuote" ], "“", [symbol]; + ["\\rdquo"; "\\rdquor"; "\\CloseCurlyDoubleQuote" ], "”", [symbol]; + ["\\ldquor" ], "„", [symbol]; + ["\\dagger" ], "†", [symbol]; + ["\\Dagger"; "\\ddagger" ], "‡", [symbol]; + ["\\nldr" ], "‥", [symbol]; + ["\\mldr"; "\\dots"; "\\ldots"; "\\hellip" ], "…", [symbol]; + ["\\prime" ], "′", [symbol]; + ["\\Prime" ], "″", [symbol]; + ["\\tprime" ], "‴", [symbol]; + ["\\bprime"; "\\backprime" ], "‵", [symbol]; + ["\\caret" ], "⁁", [symbol]; + ["\\hybull" ], "⁃", [symbol]; + ["\\bsemi" ], "⁏", [symbol]; + ["\\qprime" ], "⁗", [symbol]; + ["\\MediumSpace" ], " ", [symbol]; + ["\\tdot"; "\\TripleDot" ], "⃛", [symbol]; + ["\\DotDot" ], "⃜", [symbol]; + ["\\minus" ], "−", [symbol]; + ["\\angrt" ], "∟", [symbol]; + ["\\ang"; "\\angle" ], "∠", [symbol]; + ["\\nang" ], "∠̸", [symbol]; + ["\\angmsd"; "\\measuredangle" ], "∡", [symbol]; + ["\\angsph" ], "∢", [symbol]; + ["\\par"; "\\parallel"; "\\DoubleVerticalBar" ], "∥", [symbol]; + ["\\there4"; "\\Therefore"; "\\therefore" ], "∴", [symbol]; + ["\\becaus"; "\\because"; "\\Because" ], "∵", [symbol]; + ["\\ratio" ], "∶", [symbol]; + ["\\Colon"; "\\Proportion" ], "∷", [symbol]; + ["\\minusd"; "\\dotminus" ], "∸", [symbol]; + ["\\mDDot" ], "∺", [symbol]; + ["\\homtht" ], "∻", [symbol]; + ["\\sim"; "\\Tilde" ], "∼", [symbol]; + ["\\mstpos" ], "∾", [symbol]; + ["\\acd" ], "∿", [symbol]; + ["\\wr"; "\\wreath"; "\\VerticalTilde" ], "≀", [symbol]; + ["\\origof" ], "⊶", [symbol]; + ["\\imof" ], "⊷", [symbol]; + ["\\mumap"; "\\multimap" ], "⊸", [symbol]; + ["\\hercon" ], "⊹", [symbol]; + ["\\intcal"; "\\intercal" ], "⊺", [symbol]; + ["\\veebar" ], "⊻", [symbol]; + ["\\barwed"; "\\barwedge" ], "⊼", [symbol]; + ["\\barvee" ], "⊽", [symbol]; + ["\\vangrt" ], "⊾", [symbol]; + ["\\lrtri" ], "⊿", [symbol]; + ["\\diam"; "\\Diamond"; "\\diamond" ], "⋄", [symbol]; + ["\\sdot" ], "⋅", [symbol]; + ["\\Star"; "\\star"; "\\sstarf" ], "⋆", [symbol]; + ["\\divonx"; "\\divideontimes" ], "⋇", [symbol]; + ["\\bowtie" ], "⋈", [symbol]; + ["\\ltimes" ], "⋉", [symbol]; + ["\\rtimes" ], "⋊", [symbol]; + ["\\lthree"; "\\leftthreetimes" ], "⋋", [symbol]; + ["\\rthree"; "\\rightthreetimes" ], "⋌", [symbol]; + ["\\cuvee"; "\\curlyvee" ], "⋎", [symbol]; + ["\\cuwed"; "\\curlywedge" ], "⋏", [symbol]; + ["\\fork"; "\\pitchfork" ], "⋔", [symbol]; + ["\\epar" ], "⋕", [symbol]; + ["\\vdots"; "\\vellip" ], "⋮", [symbol]; + ["\\cdots"; "\\ctdot" ], "⋯", [symbol]; + ["\\utdot" ], "⋰", [symbol]; + ["\\ddots"; "\\dtdot" ], "⋱", [symbol]; + ["\\Barwed"; "\\doublebarwedge" ], "⌆", [symbol]; + ["\\bnot" ], "⌐", [symbol]; + ["\\profline" ], "⌒", [symbol]; + ["\\profsurf" ], "⌓", [symbol]; + ["\\telrec" ], "⌕", [symbol]; + ["\\frown" ], "⌢", [symbol]; + ["\\smile" ], "⌣", [symbol]; + ["\\blank" ], "␣", [symbol]; + ["\\HorizontalLine" ], "─", [symbol]; + ["\\loz"; "\\lozenge" ], "◊", [symbol]; + ["\\starf"; "\\bigstar" ], "★", [symbol]; + ["\\phone" ], "☎", [symbol]; + ["\\female" ], "♀", [symbol]; + ["\\male" ], "♂", [symbol]; + ["\\spades"; "\\spadesuit" ], "♠", [symbol]; + ["\\heartsuit" ], "♡", [symbol]; + ["\\diamondsuit" ], "♢", [symbol]; + ["\\clubs"; "\\clubsuit" ], "♣", [symbol]; + ["\\diams" ], "♦", [symbol]; + ["\\sung" ], "♪", [symbol]; + ["\\flat" ], "♭", [symbol]; + ["\\natur"; "\\natural" ], "♮", [symbol]; + ["\\sharp" ], "♯", [symbol]; + ["\\check"; "\\checkmark" ], "✓", [symbol]; + ["\\cross" ], "✗", [symbol]; + ["\\malt"; "\\maltese" ], "✠", [symbol]; + ["\\sext" ], "✶", [symbol]; + ["\\VerticalSeparator" ], "❘", [symbol]; + ["\\lozf"; "\\blacklozenge" ], "⧫", [symbol]; + ["\\OverParenthesis" ], "︵", [symbol]; + ["\\UnderParenthesis" ], "︶", [symbol]; + ["\\OverBrace" ], "︷", [symbol]; + ["\\UnderBrace" ], "︸", [symbol]; + ["\\Yang" ], "⚊", [symbol]; +(* }}} *) + +(* {{{ fraction *) + ["\\frac14" ], "¼", [fraction]; + ["\\half"; "\\frac" ], "½", [fraction]; + ["\\frac34" ], "¾", [fraction]; + ["\\permil" ], "‰", [fraction]; + ["\\pertenk" ], "‱", [fraction]; + ["\\incare" ], "℅", [fraction]; + ["\\frac13" ], "⅓", [fraction]; + ["\\frac23" ], "⅔", [fraction]; + ["\\frac15" ], "⅕", [fraction]; + ["\\frac25" ], "⅖", [fraction]; + ["\\frac35" ], "⅗", [fraction]; + ["\\frac45" ], "⅘", [fraction]; + ["\\frac16" ], "⅙", [fraction]; + ["\\frac56" ], "⅚", [fraction]; + ["\\frac18" ], "⅛", [fraction]; + ["\\frac38" ], "⅜", [fraction]; + ["\\frac58" ], "⅝", [fraction]; + ["\\frac78" ], "⅞", [fraction]; +(* }}} *) + +(* {{{ greek letters *) + ["\\alpha" ], "α", [greek_letter]; + ["\\beta" ], "β", [greek_letter]; + ["\\gamma" ], "γ", [greek_letter]; + ["\\delta" ], "δ", [greek_letter]; + ["\\epsilon" ], "ϵ", [greek_letter]; + ["\\varepsilon"; "\\straightepsilon" ], "ε", [greek_letter]; + ["\\epsiv" ], "ɛ", [greek_letter]; + ["\\bepsi"; "\\backepsilon" ], "϶", [greek_letter]; + ["\\zeta" ], "ζ", [greek_letter]; + ["\\eta" ], "η", [greek_letter]; + ["\\theta" ], "θ", [greek_letter]; + ["\\vartheta" ], "ϑ", [greek_letter]; + ["\\iota" ], "ι", [greek_letter]; + ["\\kappa" ], "κ", [greek_letter]; + ["\\varkappa" ], "ϰ", [greek_letter]; + ["\\lambda" ], "λ", [greek_letter]; + ["\\mu" ], "μ", [greek_letter]; + ["\\nu" ], "ν", [greek_letter]; + ["\\xi" ], "ξ", [greek_letter]; + ["\\o" ], "ο", [greek_letter]; + ["\\pi" ], "π", [greek_letter]; + ["\\varpi" ], "ϖ", [greek_letter]; + ["\\rho" ], "ρ", [greek_letter]; + ["\\varrho" ], "ϱ", [greek_letter]; + ["\\sigma" ], "σ", [greek_letter]; + ["\\varsigma" ], "ς", [greek_letter]; + ["\\tau" ], "τ", [greek_letter]; + ["\\upsilon" ], "υ", [greek_letter]; + ["\\phi" ], "ϕ", [greek_letter]; + ["\\varphi"; "\\straightphi" ], "φ", [greek_letter]; + ["\\chi" ], "χ", [greek_letter]; + ["\\psi" ], "ψ", [greek_letter]; + ["\\omega" ], "ω", [greek_letter]; + ["\\Gamma" ], "Γ", [greek_letter]; + ["\\Gammad"; "\\gammad"; "\\digamma" ], "Ϝ", [greek_letter]; + ["\\Delta" ], "Δ", [greek_letter]; + ["\\Theta" ], "Θ", [greek_letter]; + ["\\Lambda" ], "Λ", [greek_letter]; + ["\\Xi" ], "Ξ", [greek_letter]; + ["\\Pi" ], "Π", [greek_letter]; + ["\\Sigma" ], "Σ", [greek_letter]; + ["\\Upsilon" ], "ϒ", [greek_letter]; + ["\\Phi" ], "Φ", [greek_letter]; + ["\\Psi" ], "Ψ", [greek_letter]; + ["\\Omega" ], "Ω", [greek_letter]; +(* }}} *) + +(* {{{ letters *) + ["\\iexcl" ], "¡", [letter]; + ["\\ordf" ], "ª", [letter]; + ["\\micro" ], "µ", [letter]; + ["\\Agrave" ], "À", [letter]; + ["\\Aacute" ], "Á", [letter]; + ["\\Acirc" ], "Â", [letter]; + ["\\Atilde" ], "Ã", [letter]; + ["\\Auml" ], "Ä", [letter]; + ["\\Aring" ], "Å", [letter]; + ["\\AElig" ], "Æ", [letter]; + ["\\Ccedil" ], "Ç", [letter]; + ["\\Egrave" ], "È", [letter]; + ["\\Eacute" ], "É", [letter]; + ["\\Ecirc" ], "Ê", [letter]; + ["\\Euml" ], "Ë", [letter]; + ["\\Igrave" ], "Ì", [letter]; + ["\\Iacute" ], "Í", [letter]; + ["\\Icirc" ], "Î", [letter]; + ["\\Iuml" ], "Ï", [letter]; + ["\\ETH" ], "Ð", [letter]; + ["\\Ntilde" ], "Ñ", [letter]; + ["\\Ograve" ], "Ò", [letter]; + ["\\Oacute" ], "Ó", [letter]; + ["\\Ocirc" ], "Ô", [letter]; + ["\\Otilde" ], "Õ", [letter]; + ["\\Ouml" ], "Ö", [letter]; + ["\\Oslash" ], "Ø", [letter]; + ["\\Ugrave" ], "Ù", [letter]; + ["\\Uacute" ], "Ú", [letter]; + ["\\Ucirc" ], "Û", [letter]; + ["\\Uuml" ], "Ü", [letter]; + ["\\Yacute" ], "Ý", [letter]; + ["\\THORN" ], "Þ", [letter]; + ["\\szlig" ], "ß", [letter]; + ["\\agrave" ], "à", [letter]; + ["\\aacute" ], "á", [letter]; + ["\\acirc" ], "â", [letter]; + ["\\atilde" ], "ã", [letter]; + ["\\auml" ], "ä", [letter]; + ["\\aring" ], "å", [letter]; + ["\\aelig" ], "æ", [letter]; + ["\\ccedil" ], "ç", [letter]; + ["\\egrave" ], "è", [letter]; + ["\\eacute" ], "é", [letter]; + ["\\ecirc" ], "ê", [letter]; + ["\\euml" ], "ë", [letter]; + ["\\igrave" ], "ì", [letter]; + ["\\iacute" ], "í", [letter]; + ["\\icirc" ], "î", [letter]; + ["\\iuml" ], "ï", [letter]; + ["\\eth" ], "ð", [letter]; + ["\\ntilde" ], "ñ", [letter]; + ["\\ograve" ], "ò", [letter]; + ["\\oacute" ], "ó", [letter]; + ["\\ocirc" ], "ô", [letter]; + ["\\otilde" ], "õ", [letter]; + ["\\ouml" ], "ö", [letter]; + ["\\ugrave" ], "ù", [letter]; + ["\\uacute" ], "ú", [letter]; + ["\\ucirc" ], "û", [letter]; + ["\\uuml" ], "ü", [letter]; + ["\\yacute" ], "ý", [letter]; + ["\\yuml" ], "ÿ", [letter]; + ["\\Amacr" ], "Ā", [letter]; + ["\\amacr" ], "ā", [letter]; + ["\\Abreve" ], "Ă", [letter]; + ["\\abreve" ], "ă", [letter]; + ["\\Aogon" ], "Ą", [letter]; + ["\\aogon" ], "ą", [letter]; + ["\\Cacute" ], "Ć", [letter]; + ["\\cacute" ], "ć", [letter]; + ["\\Ccirc" ], "Ĉ", [letter]; + ["\\ccirc" ], "ĉ", [letter]; + ["\\Cdot" ], "Ċ", [letter]; + ["\\cdot" ], "ċ", [letter]; + ["\\Ccaron" ], "Č", [letter]; + ["\\ccaron" ], "č", [letter]; + ["\\Dcaron" ], "Ď", [letter]; + ["\\dcaron" ], "ď", [letter]; + ["\\Dstrok" ], "Đ", [letter]; + ["\\dstrok" ], "đ", [letter]; + ["\\Emacr" ], "Ē", [letter]; + ["\\emacr" ], "ē", [letter]; + ["\\Edot" ], "Ė", [letter]; + ["\\edot" ], "ė", [letter]; + ["\\Eogon" ], "Ę", [letter]; + ["\\eogon" ], "ę", [letter]; + ["\\Ecaron" ], "Ě", [letter]; + ["\\ecaron" ], "ě", [letter]; + ["\\Gcirc" ], "Ĝ", [letter]; + ["\\gcirc" ], "ĝ", [letter]; + ["\\Gbreve" ], "Ğ", [letter]; + ["\\gbreve" ], "ğ", [letter]; + ["\\Gdot" ], "Ġ", [letter]; + ["\\gdot" ], "ġ", [letter]; + ["\\Gcedil" ], "Ģ", [letter]; + ["\\Hcirc" ], "Ĥ", [letter]; + ["\\hcirc" ], "ĥ", [letter]; + ["\\Hstrok" ], "Ħ", [letter]; + ["\\hstrok" ], "ħ", [letter]; + ["\\Itilde" ], "Ĩ", [letter]; + ["\\itilde" ], "ĩ", [letter]; + ["\\Imacr" ], "Ī", [letter]; + ["\\imacr" ], "ī", [letter]; + ["\\Iogon" ], "Į", [letter]; + ["\\iogon" ], "į", [letter]; + ["\\Idot" ], "İ", [letter]; + ["\\IJlig" ], "IJ", [letter]; + ["\\ijlig" ], "ij", [letter]; + ["\\Jcirc" ], "Ĵ", [letter]; + ["\\jcirc" ], "ĵ", [letter]; + ["\\Kcedil" ], "Ķ", [letter]; + ["\\kcedil" ], "ķ", [letter]; + ["\\kgreen" ], "ĸ", [letter]; + ["\\Lacute" ], "Ĺ", [letter]; + ["\\lacute" ], "ĺ", [letter]; + ["\\Lcedil" ], "Ļ", [letter]; + ["\\lcedil" ], "ļ", [letter]; + ["\\Lcaron" ], "Ľ", [letter]; + ["\\lcaron" ], "ľ", [letter]; + ["\\Lmidot" ], "Ŀ", [letter]; + ["\\lmidot" ], "ŀ", [letter]; + ["\\Lstrok" ], "Ł", [letter]; + ["\\lstrok" ], "ł", [letter]; + ["\\Nacute" ], "Ń", [letter]; + ["\\nacute" ], "ń", [letter]; + ["\\Ncedil" ], "Ņ", [letter]; + ["\\ncedil" ], "ņ", [letter]; + ["\\Ncaron" ], "Ň", [letter]; + ["\\ncaron" ], "ň", [letter]; + ["\\napos" ], "ʼn", [letter]; + ["\\ENG" ], "Ŋ", [letter]; + ["\\eng" ], "ŋ", [letter]; + ["\\Omacr" ], "Ō", [letter]; + ["\\omacr" ], "ō", [letter]; + ["\\Odblac" ], "Ő", [letter]; + ["\\odblac" ], "ő", [letter]; + ["\\OElig" ], "Œ", [letter]; + ["\\oelig" ], "œ", [letter]; + ["\\Racute" ], "Ŕ", [letter]; + ["\\racute" ], "ŕ", [letter]; + ["\\Rcedil" ], "Ŗ", [letter]; + ["\\rcedil" ], "ŗ", [letter]; + ["\\Rcaron" ], "Ř", [letter]; + ["\\rcaron" ], "ř", [letter]; + ["\\Sacute" ], "Ś", [letter]; + ["\\sacute" ], "ś", [letter]; + ["\\Scirc" ], "Ŝ", [letter]; + ["\\scirc" ], "ŝ", [letter]; + ["\\Scedil" ], "Ş", [letter]; + ["\\scedil" ], "ş", [letter]; + ["\\Scaron" ], "Š", [letter]; + ["\\scaron" ], "š", [letter]; + ["\\Tcedil" ], "Ţ", [letter]; + ["\\tcedil" ], "ţ", [letter]; + ["\\Tcaron" ], "Ť", [letter]; + ["\\tcaron" ], "ť", [letter]; + ["\\Tstrok" ], "Ŧ", [letter]; + ["\\tstrok" ], "ŧ", [letter]; + ["\\Utilde" ], "Ũ", [letter]; + ["\\utilde" ], "ũ", [letter]; + ["\\Umacr" ], "Ū", [letter]; + ["\\umacr" ], "ū", [letter]; + ["\\Ubreve" ], "Ŭ", [letter]; + ["\\ubreve" ], "ŭ", [letter]; + ["\\Uring" ], "Ů", [letter]; + ["\\uring" ], "ů", [letter]; + ["\\Udblac" ], "Ű", [letter]; + ["\\udblac" ], "ű", [letter]; + ["\\Uogon" ], "Ų", [letter]; + ["\\uogon" ], "ų", [letter]; + ["\\Wcirc" ], "Ŵ", [letter]; + ["\\wcirc" ], "ŵ", [letter]; + ["\\Ycirc" ], "Ŷ", [letter]; + ["\\ycirc" ], "ŷ", [letter]; + ["\\Yuml" ], "Ÿ", [letter]; + ["\\Zacute" ], "Ź", [letter]; + ["\\zacute" ], "ź", [letter]; + ["\\Zdot" ], "Ż", [letter]; + ["\\zdot" ], "ż", [letter]; + ["\\Zcaron" ], "Ž", [letter]; + ["\\zcaron" ], "ž", [letter]; + ["\\fnof" ], "ƒ", [letter]; + ["\\gacute" ], "ǵ", [letter]; + ["\\IOcy" ], "Ё", [letter]; + ["\\DJcy" ], "Ђ", [letter]; + ["\\GJcy" ], "Ѓ", [letter]; + ["\\Jukcy" ], "Є", [letter]; + ["\\DScy" ], "Ѕ", [letter]; + ["\\Iukcy" ], "І", [letter]; + ["\\YIcy" ], "Ї", [letter]; + ["\\Jsercy" ], "Ј", [letter]; + ["\\LJcy" ], "Љ", [letter]; + ["\\NJcy" ], "Њ", [letter]; + ["\\TSHcy" ], "Ћ", [letter]; + ["\\KJcy" ], "Ќ", [letter]; + ["\\Ubrcy" ], "Ў", [letter]; + ["\\DZcy" ], "Џ", [letter]; + ["\\Acy" ], "А", [letter]; + ["\\Bcy" ], "Б", [letter]; + ["\\Vcy" ], "В", [letter]; + ["\\Gcy" ], "Г", [letter]; + ["\\Dcy" ], "Д", [letter]; + ["\\IEcy" ], "Е", [letter]; + ["\\ZHcy" ], "Ж", [letter]; + ["\\Zcy" ], "З", [letter]; + ["\\Icy" ], "И", [letter]; + ["\\Jcy" ], "Й", [letter]; + ["\\Kcy" ], "К", [letter]; + ["\\Lcy" ], "Л", [letter]; + ["\\Mcy" ], "М", [letter]; + ["\\Ncy" ], "Н", [letter]; + ["\\Ocy" ], "О", [letter]; + ["\\Pcy" ], "П", [letter]; + ["\\Rcy" ], "Р", [letter]; + ["\\Scy" ], "С", [letter]; + ["\\Tcy" ], "Т", [letter]; + ["\\Ucy" ], "У", [letter]; + ["\\Fcy" ], "Ф", [letter]; + ["\\KHcy" ], "Х", [letter]; + ["\\TScy" ], "Ц", [letter]; + ["\\CHcy" ], "Ч", [letter]; + ["\\SHcy" ], "Ш", [letter]; + ["\\SHCHcy" ], "Щ", [letter]; + ["\\HARDcy" ], "Ъ", [letter]; + ["\\Ycy" ], "Ы", [letter]; + ["\\SOFTcy" ], "Ь", [letter]; + ["\\Ecy" ], "Э", [letter]; + ["\\YUcy" ], "Ю", [letter]; + ["\\YAcy" ], "Я", [letter]; + ["\\acy" ], "а", [letter]; + ["\\bcy" ], "б", [letter]; + ["\\vcy" ], "в", [letter]; + ["\\gcy" ], "г", [letter]; + ["\\dcy" ], "д", [letter]; + ["\\iecy" ], "е", [letter]; + ["\\zhcy" ], "ж", [letter]; + ["\\zcy" ], "з", [letter]; + ["\\icy" ], "и", [letter]; + ["\\jcy" ], "й", [letter]; + ["\\kcy" ], "к", [letter]; + ["\\lcy" ], "л", [letter]; + ["\\mcy" ], "м", [letter]; + ["\\ncy" ], "н", [letter]; + ["\\ocy" ], "о", [letter]; + ["\\pcy" ], "п", [letter]; + ["\\rcy" ], "р", [letter]; + ["\\scy" ], "с", [letter]; + ["\\tcy" ], "т", [letter]; + ["\\ucy" ], "у", [letter]; + ["\\fcy" ], "ф", [letter]; + ["\\khcy" ], "х", [letter]; + ["\\tscy" ], "ц", [letter]; + ["\\chcy" ], "ч", [letter]; + ["\\shcy" ], "ш", [letter]; + ["\\shchcy" ], "щ", [letter]; + ["\\hardcy" ], "ъ", [letter]; + ["\\ycy" ], "ы", [letter]; + ["\\softcy" ], "ь", [letter]; + ["\\ecy" ], "э", [letter]; + ["\\yucy" ], "ю", [letter]; + ["\\yacy" ], "я", [letter]; + ["\\iocy" ], "ё", [letter]; + ["\\djcy" ], "ђ", [letter]; + ["\\gjcy" ], "ѓ", [letter]; + ["\\jukcy" ], "є", [letter]; + ["\\dscy" ], "ѕ", [letter]; + ["\\iukcy" ], "і", [letter]; + ["\\yicy" ], "ї", [letter]; + ["\\jsercy" ], "ј", [letter]; + ["\\ljcy" ], "љ", [letter]; + ["\\njcy" ], "њ", [letter]; + ["\\tshcy" ], "ћ", [letter]; + ["\\kjcy" ], "ќ", [letter]; + ["\\ubrcy" ], "ў", [letter]; + ["\\dzcy" ], "џ", [letter]; + ["\\Copf"; "\\complexes" ], "ℂ", [letter]; + ["\\gscr" ], "ℊ", [letter]; + ["\\Hscr"; "\\hamilt"; "\\HilbertSpace" ], "ℋ", [letter]; + ["\\Hfr"; "\\Poincareplane" ], "ℌ", [letter]; + ["\\Hopf"; "\\quaternions" ], "ℍ", [letter]; + ["\\planckh" ], "ℎ", [letter]; + ["\\hslash"; "\\plankv" ], "ℏ", [letter]; + ["\\hbar"; "\\planck" ], "ℏ︀", [letter]; + ["\\Iscr"; "\\imagline" ], "ℐ", [letter]; + ["\\Im"; "\\Ifr"; "\\image"; "\\imagpart" ], "ℑ", [letter]; + ["\\Lscr"; "\\lagran"; "\\Laplacetrf" ], "ℒ", [letter]; + ["\\ell"; "\\lscr" ], "ℓ", [letter]; + ["\\Nopf"; "\\naturals" ], "ℕ", [letter]; + ["\\numero" ], "№", [letter]; + ["\\copysr" ], "℗", [letter]; + ["\\wp"; "\\weierp" ], "℘", [letter]; + ["\\Popf"; "\\primes" ], "ℙ", [letter]; + ["\\Qopf"; "\\rationals" ], "ℚ", [letter]; + ["\\Rscr"; "\\realine" ], "ℛ", [letter]; + ["\\Re"; "\\Rfr"; "\\real"; "\\realpart" ], "ℜ", [letter]; + ["\\Ropf"; "\\reals" ], "ℝ", [letter]; + ["\\rx" ], "℞", [letter]; + ["\\trade" ], "™", [letter]; + ["\\Zopf"; "\\integers" ], "ℤ", [letter]; + ["\\ohm" ], "Ω", [letter]; + ["\\mho" ], "℧", [letter]; + ["\\Zfr"; "\\zeetrf" ], "ℨ", [letter]; + ["\\iiota" ], "℩", [letter]; + ["\\angst" ], "Å", [letter]; + ["\\Bscr"; "\\bernou"; "\\Bernoullis" ], "ℬ", [letter]; + ["\\Cfr"; "\\Cayleys" ], "ℭ", [letter]; + ["\\escr" ], "ℯ", [letter]; + ["\\Escr"; "\\expectation" ], "ℰ", [letter]; + ["\\Fscr"; "\\Fouriertrf" ], "ℱ", [letter]; + ["\\Mscr"; "\\phmmat"; "\\Mellintrf" ], "ℳ", [letter]; + ["\\oscr"; "\\order"; "\\orderof" ], "ℴ", [letter]; + ["\\aleph" ], "ℵ", [letter]; + ["\\beth" ], "ℶ", [letter]; + ["\\gimel" ], "ℷ", [letter]; + ["\\daleth" ], "ℸ", [letter]; + ["\\DD"; "\\CapitalDifferentialD" ], "ⅅ", [letter]; + ["\\dd"; "\\DifferentialD" ], "ⅆ", [letter]; + ["\\ee"; "\\exponentiale"; "\\ExponentialE" ], "ⅇ", [letter]; + ["\\ii"; "\\ImaginaryI" ], "ⅈ", [letter]; + ["\\comp"; "\\complement" ], "∁", [letter]; + ["\\part"; "\\partial"; "\\PartialD" ], "∂", [letter]; + ["\\npart" ], "∂̸", [letter]; + ["\\easter" ], "≛", [letter]; + ["\\fpartint" ], "⨍", [letter]; + ["\\fflig" ], "ff", [letter]; + ["\\filig" ], "fi", [letter]; + ["\\fllig" ], "fl", [letter]; + ["\\ffilig" ], "ffi", [letter]; + ["\\ffllig" ], "ffl", [letter]; + ["\\Aopf" ], "𝔸", [letter]; + ["\\Bopf" ], "𝔹", [letter]; + ["\\Dopf" ], "𝔻", [letter]; + ["\\Eopf" ], "𝔼", [letter]; + ["\\Fopf" ], "𝔽", [letter]; + ["\\Gopf" ], "𝔾", [letter]; + ["\\Iopf" ], "𝕀", [letter]; + ["\\Jopf" ], "𝕁", [letter]; + ["\\Kopf" ], "𝕂", [letter]; + ["\\Lopf"; "\\imped" ], "𝕃", [letter]; + ["\\Mopf" ], "𝕄", [letter]; + ["\\Oopf" ], "𝕆", [letter]; + ["\\Sopf" ], "𝕊", [letter]; + ["\\Topf" ], "𝕋", [letter]; + ["\\Uopf" ], "𝕌", [letter]; + ["\\Vopf" ], "𝕍", [letter]; + ["\\Wopf" ], "𝕎", [letter]; + ["\\Xopf" ], "𝕏", [letter]; + ["\\Yopf" ], "𝕐", [letter]; + ["\\aopf" ], "𝕒", [letter]; + ["\\bopf" ], "𝕓", [letter]; + ["\\copf" ], "𝕔", [letter]; + ["\\dopf" ], "𝕕", [letter]; + ["\\eopf" ], "𝕖", [letter]; + ["\\fopf" ], "𝕗", [letter]; + ["\\gopf" ], "𝕘", [letter]; + ["\\hopf" ], "𝕙", [letter]; + ["\\iopf" ], "𝕚", [letter]; + ["\\jopf" ], "𝕛", [letter]; + ["\\kopf" ], "𝕜", [letter]; + ["\\lopf" ], "𝕝", [letter]; + ["\\mopf" ], "𝕞", [letter]; + ["\\nopf" ], "𝕟", [letter]; + ["\\oopf" ], "𝕠", [letter]; + ["\\popf" ], "𝕡", [letter]; + ["\\qopf" ], "𝕢", [letter]; + ["\\ropf" ], "𝕣", [letter]; + ["\\sopf" ], "𝕤", [letter]; + ["\\topf" ], "𝕥", [letter]; + ["\\uopf" ], "𝕦", [letter]; + ["\\vopf" ], "𝕧", [letter]; + ["\\wopf" ], "𝕨", [letter]; + ["\\xopf" ], "𝕩", [letter]; + ["\\yopf" ], "𝕪", [letter]; + ["\\zopf" ], "𝕫", [letter]; +(* }}} *) + +(* {{{ ASCII art *) + ["\\lceil"; "\\LeftCeiling" ], "⌈", [asciiart]; + ["\\rceil"; "\\RightCeiling" ], "⌉", [asciiart]; + ["\\lfloor"; "\\LeftFloor" ], "⌊", [asciiart]; + ["\\rfloor"; "\\RightFloor" ], "⌋", [asciiart]; + ["\\drcrop" ], "⌌", [asciiart]; + ["\\dlcrop" ], "⌍", [asciiart]; + ["\\urcrop" ], "⌎", [asciiart]; + ["\\ulcrop" ], "⌏", [asciiart]; + ["\\ulcorn"; "\\ulcorner" ], "⌜", [asciiart]; + ["\\urcorn"; "\\urcorner" ], "⌝", [asciiart]; + ["\\dlcorn"; "\\llcorner" ], "⌞", [asciiart]; + ["\\drcorn"; "\\lrcorner" ], "⌟", [asciiart]; + ["\\boxh" ], "─", [asciiart]; + ["\\boxv" ], "│", [asciiart]; + ["\\boxdr" ], "┌", [asciiart]; + ["\\boxdl" ], "┐", [asciiart]; + ["\\boxur" ], "└", [asciiart]; + ["\\boxul" ], "┘", [asciiart]; + ["\\boxvr" ], "├", [asciiart]; + ["\\boxvl" ], "┤", [asciiart]; + ["\\boxhd" ], "┬", [asciiart]; + ["\\boxhu" ], "┴", [asciiart]; + ["\\boxvh" ], "┼", [asciiart]; + ["\\boxH" ], "═", [asciiart]; + ["\\boxV" ], "║", [asciiart]; + ["\\boxdR" ], "╒", [asciiart]; + ["\\boxDr" ], "╓", [asciiart]; + ["\\boxDR" ], "╔", [asciiart]; + ["\\boxdL" ], "╕", [asciiart]; + ["\\boxDl" ], "╖", [asciiart]; + ["\\boxDL" ], "╗", [asciiart]; + ["\\boxuR" ], "╘", [asciiart]; + ["\\boxUr" ], "╙", [asciiart]; + ["\\boxUR" ], "╚", [asciiart]; + ["\\boxuL" ], "╛", [asciiart]; + ["\\boxUl" ], "╜", [asciiart]; + ["\\boxUL" ], "╝", [asciiart]; + ["\\boxvR" ], "╞", [asciiart]; + ["\\boxVr" ], "╟", [asciiart]; + ["\\boxVR" ], "╠", [asciiart]; + ["\\boxvL" ], "╡", [asciiart]; + ["\\boxVl" ], "╢", [asciiart]; + ["\\boxVL" ], "╣", [asciiart]; + ["\\boxHd" ], "╤", [asciiart]; + ["\\boxhD" ], "╥", [asciiart]; + ["\\boxHD" ], "╦", [asciiart]; + ["\\boxHu" ], "╧", [asciiart]; + ["\\boxhU" ], "╨", [asciiart]; + ["\\boxHU" ], "╩", [asciiart]; + ["\\boxvH" ], "╪", [asciiart]; + ["\\boxVh" ], "╫", [asciiart]; + ["\\boxVH" ], "╬", [asciiart]; + ["\\block" ], "█", [asciiart]; + ["\\blk14" ], "░", [asciiart]; + ["\\blk12" ], "▒", [asciiart]; + ["\\blk34" ], "▓", [asciiart]; +(* }}} *) + +(* {{{ equivalence *) + ["\\bsim"; "\\backsim" ], "∽", [equivalence]; + ["\\nsim"; "\\NotTilde" ], "≁", [equivalence]; + ["\\nvsim" ], "≁̸", [equivalence]; + ["\\esim"; "\\eqsim"; "\\EqualTilde" ], "≂", [equivalence]; + ["\\nesim"; "\\NotEqualTilde" ], "≂̸", [equivalence]; + ["\\sime"; "\\simeq"; "\\TildeEqual" ], "≃", [equivalence]; + ["\\nsime"; "\\nsimeq"; "\\NotTildeEqual" ], "≄", [equivalence]; + ["\\cong"; "\\TildeFullEqual" ], "≅", [equivalence]; + ["\\simne" ], "≆", [equivalence]; + ["\\ncong"; "\\NotTildeFullEqual" ], "≇", [equivalence]; + ["\\ap"; "\\approx"; "\\TildeTilde" ], "≈", [equivalence]; + ["\\nap"; "\\napprox"; "\\NotTildeTilde" ], "≉", [equivalence]; + ["\\nvap" ], "≉̸", [equivalence]; + ["\\apE"; "\\ape"; "\\approxeq" ], "≊", [equivalence]; + ["\\apid" ], "≋", [equivalence]; + ["\\napid" ], "≋̸", [equivalence]; + ["\\bcong"; "\\backcong" ], "≌", [equivalence]; + ["\\asymp"; "\\CupCap" ], "≍", [equivalence]; + ["\\bump"; "\\Bumpeq"; "\\HumpDownHump" ], "≎", [equivalence]; + ["\\nbump"; "\\NotHumpDownHump" ], "≎̸", [equivalence]; + ["\\bumpe"; "\\bumpeq"; "\\HumpEqual" ], "≏", [equivalence]; + ["\\nbumpe"; "\\NotHumpEqual" ], "≏̸", [equivalence]; + ["\\esdot"; "\\doteq"; "\\DotEqual" ], "≐", [equivalence]; + ["\\eDot"; "\\doteqdot" ], "≑", [equivalence]; + ["\\efDot"; "\\fallingdotseq" ], "≒", [equivalence]; + ["\\erDot"; "\\risingdotseq" ], "≓", [equivalence]; + ["\\colone"; "\\Assign"; "\\coloneq" ], "≔", [equivalence]; + ["\\ecolon"; "\\eqcolon" ], "≕", [equivalence]; + ["\\ecir"; "\\eqcirc" ], "≖", [equivalence]; + ["\\cire"; "\\circeq" ], "≗", [equivalence]; + ["\\wedgeq" ], "≙", [equivalence]; + ["\\veeeq" ], "≚", [equivalence]; + ["\\trie"; "\\triangleq" ], "≜", [equivalence]; + ["\\def";"\\:=" ], "≝", [equivalence]; + ["\\equest"; "\\questeq" ], "≟", [equivalence]; + ["\\ne"; "\\neq"; "\\NotEqual" ], "≠", [equivalence]; + ["\\equiv"; "\\Congruent" ], "≡", [equivalence]; + ["\\nequiv"; "\\NotCongruent" ], "≢", [equivalence]; + ["\\NotCupCap" ], "≭", [equivalence]; + ["\\bsime"; "\\backsimeq" ], "⋍", [equivalence]; + ["\\bumpE" ], "⪮", [equivalence]; +(* }}} *) + +(* {{{ order *) + ["\\le"; "\\leq";"\\<=" ], "≤", [order]; + ["\\ge"; "\\geq"; "\\GreaterEqual";"\\>=" ], "≥", [order]; + ["\\lE"; "\\leqq"; "\\LessFullEqual" ], "≦", [order]; + ["\\gE"; "\\geqq"; "\\GreaterFullEqual" ], "≧", [order]; + ["\\lnE"; "\\lne"; "\\lneq"; "\\lneqq" ], "≨", [order]; + ["\\gnE"; "\\gne"; "\\gneq"; "\\gneqq" ], "≩", [order]; + ["\\Lt"; "\\ll"; "\\NestedLessLess" ], "≪", [order]; + ["\\nLt" ], "≪̸", [order]; + ["\\gg"; "\\Gt"; "\\NestedGreaterGreater" ], "≫", [order]; + ["\\nGt" ], "≫̸", [order]; + ["\\nlt"; "\\nvlt"; "\\nless"; "\\NotLess" ], "≮", [order]; + ["\\ngt"; "\\ngtr"; "\\nvgt"; "\\NotGreater" ], "≯", [order]; + ["\\nlE"; "\\nleq"; "\\nvle"; "\\nles"; "\\nleqq"; "\\nleqslant"; "\\NotLessSlantEqual"; "\\NotGreaterFullEqual"], "≰", [order]; + ["\\ngE"; "\\nges"; "\\nvge"; "\\ngeq"; "\\ngeqq"; "\\ngeqslant"; "\\NotGreaterSlantEqual"], "≱", [order]; + ["\\lap"; "\\lsim"; "\\lesssim"; "\\LessTilde"; "\\lessapprox" ], "≲", [order]; + ["\\gap"; "\\gsim"; "\\gtrsim"; "\\gtrapprox"; "\\GreaterTilde" ], "≳", [order]; + ["\\nlsim"; "\\NotLessTilde" ], "≴", [order]; + ["\\ngsim"; "\\NotGreaterTilde" ], "≵", [order]; + ["\\lessgtr"; "\\LessGreater" ], "≶", [order]; + ["\\gl"; "\\gtrless"; "\\GreaterLess" ], "≷", [order]; + ["\\ntlg"; "\\NotLessGreater" ], "≸", [order]; + ["\\ntgl"; "\\NotGreaterLess" ], "≹", [order]; + ["\\pr"; "\\prec"; "\\Precedes" ], "≺", [order]; + ["\\sc"; "\\succ"; "\\Succeeds" ], "≻", [order]; + ["\\prcue"; "\\preccurlyeq"; "\\PrecedesSlantEqual" ], "≼", [order]; + ["\\sce"; "\\sccue"; "\\succeq"; "\\succcurlyeq"; "\\SucceedsEqual"; "\\SucceedsSlantEqual"], "≽", [order]; + ["\\scE"; "\\prap"; "\\prsim"; "\\precsim"; "\\precapprox"; "\\PrecedesTilde"], "≾", [order]; + ["\\scap"; "\\scsim"; "\\succsim"; "\\succapprox"; "\\SucceedsTilde"], "≿", [order]; + ["\\NotSucceedsTilde" ], "≿̸", [order]; + ["\\npr"; "\\nprec"; "\\NotPrecedes" ], "⊀", [order]; + ["\\nsc"; "\\nsucc"; "\\NotSucceeds" ], "⊁", [order]; + ["\\ltdot"; "\\lessdot" ], "⋖", [order]; + ["\\gtdot"; "\\gtrdot" ], "⋗", [order]; + ["\\Ll" ], "⋘", [order]; + ["\\nLl" ], "⋘̸", [order]; + ["\\Gg"; "\\ggg" ], "⋙", [order]; + ["\\nGg" ], "⋙̸", [order]; + ["\\lEg"; "\\leg"; "\\lesseqgtr"; "\\lesseqqgtr"; "\\LessEqualGreater"], "⋚", [order]; + ["\\gEl"; "\\gel"; "\\gtreqless"; "\\gtreqqless"; "\\GreaterEqualLess"], "⋛", [order]; + ["\\els"; "\\eqslantless" ], "⋜", [order]; + ["\\egs"; "\\eqslantgtr" ], "⋝", [order]; + ["\\cuepr"; "\\curlyeqprec" ], "⋞", [order]; + ["\\cuesc"; "\\curlyeqsucc" ], "⋟", [order]; + ["\\nprcue"; "\\NotPrecedesSlantEqual" ], "⋠", [order]; + ["\\nsccue"; "\\NotSucceedsSlantEqual" ], "⋡", [order]; + ["\\lnsim" ], "⋦", [order]; + ["\\gnsim" ], "⋧", [order]; + ["\\prnap"; "\\prnsim"; "\\precnsim"; "\\precnapprox" ], "⋨", [order]; + ["\\scnap"; "\\scnsim"; "\\succnsim"; "\\succnapprox" ], "⋩", [order]; + ["\\gtrarr" ], "⥸", [order]; + ["\\les"; "\\leqslant"; "\\LessSlantEqual" ], "⩽", [order]; + ["\\ges"; "\\geqslant"; "\\GreaterSlantEqual" ], "⩾", [order]; + ["\\lesdot" ], "⩿", [order]; + ["\\gesdot" ], "⪀", [order]; + ["\\lesdoto" ], "⪁", [order]; + ["\\gesdoto" ], "⪂", [order]; + ["\\lesdotor" ], "⪃", [order]; + ["\\gesdotol" ], "⪄", [order]; + ["\\lnap"; "\\lnapprox" ], "⪉", [order]; + ["\\gnap"; "\\gnapprox" ], "⪊", [order]; + ["\\lsime" ], "⪍", [order]; + ["\\gsime" ], "⪎", [order]; + ["\\lsimg" ], "⪏", [order]; + ["\\gsiml" ], "⪐", [order]; + ["\\lgE" ], "⪑", [order]; + ["\\glE" ], "⪒", [order]; + ["\\lesges" ], "⪓", [order]; + ["\\gesles" ], "⪔", [order]; + ["\\elsdot" ], "⪗", [order]; + ["\\egsdot" ], "⪘", [order]; + ["\\el" ], "⪙", [order]; + ["\\eg" ], "⪚", [order]; + ["\\siml" ], "⪝", [order]; + ["\\simg" ], "⪞", [order]; + ["\\simlE" ], "⪟", [order]; + ["\\simgE" ], "⪠", [order]; + ["\\prE"; "\\pre"; "\\preceq"; "\\PrecedesEqual" ], "⪯", [order]; + ["\\npre"; "\\npreceq"; "\\NotPrecedesEqual" ], "⪯̸", [order]; + ["\\nsce"; "\\nsucceq"; "\\NotSucceedsEqual" ], "⪰̸", [order]; + ["\\prnE"; "\\precneqq" ], "⪵", [order]; + ["\\scnE"; "\\succneqq" ], "⪶", [order]; +(* }}} *) + +(* {{{ circles *) + ["\\copy" ], "©", [circle]; + ["\\reg"; "\\circledR" ], "®", [circle]; + ["\\ordm" ], "º", [circle]; + ["\\oslash" ], "ø", [circle]; + ["\\ring" ], "˚", [circle]; + ["\\bull"; "\\bullet" ], "•", [circle]; + ["\\circ"; "\\compfn"; "\\SmallCircle" ], "∘", [circle]; + ["\\oplus"; "\\xoplus"; "\\bigoplus"; "\\CirclePlus" ], "⊕", [circle]; + ["\\ominus"; "\\CircleMinus" ], "⊖", [circle]; + ["\\xotime"; "\\otimes"; "\\bigotimes"; "\\CircleTimes"], "⊗", [circle]; + ["\\osol" ], "⊘", [circle]; + ["\\odot"; "\\xodot"; "\\bigodot"; "\\CircleDot" ], "⊙", [circle]; + ["\\ocir"; "\\circledcirc" ], "⊚", [circle]; + ["\\oast"; "\\circledast" ], "⊛", [circle]; + ["\\odash"; "\\circleddash" ], "⊝", [circle]; + ["\\ovbar" ], "⌽", [circle]; + ["\\NotNestedLessLess" ], "⒡̸", [circle]; + ["\\NotNestedGreaterGreater" ], "⒢̸", [circle]; + ["\\oS"; "\\circledS" ], "Ⓢ", [circle]; + ["\\cir"; ], "○", [circle]; + ["\\xcirc"; "\\bigcirc" ], "◯", [circle]; +(* }}} *) + +(* {{{ squares *) + ["\\plusb"; "\\boxplus" ], "⊞", [square]; + ["\\minusb"; "\\boxminus" ], "⊟", [square]; + ["\\timesb"; "\\boxtimes" ], "⊠", [square]; + ["\\sdotb"; "\\dotsquare" ], "⊡", [square]; + ["\\uhblk" ], "▀", [square]; + ["\\lhblk" ], "▄", [square]; + ["\\squ"; "\\square"; "\\Square" ], "□", [square]; + ["\\squf"; "\\squarf"; "\\blacksquare" ], "▪", [square]; + ["\\rect" ], "▭", [square]; + ["\\marker" ], "▮", [square]; + ["\\EmptySmallSquare" ], "◽", [square]; + ["\\FilledSmallSquare" ], "◾", [square]; +(* }}} *) + +(* {{{ triangles *) + ["\\Del"; "\\nabla" ], "∇", [triangle]; + ["\\vltri"; "\\LeftTriangle"; "\\vartriangleleft" ], "⊲", [triangle]; + ["\\vrtri"; "\\RightTriangle"; "\\vartriangleright" ], "⊳", [triangle]; + ["\\ltrie"; "\\trianglelefteq"; "\\LeftTriangleEqual" ], "⊴", [triangle]; + ["\\rtrie"; "\\trianglerighteq"; "\\RightTriangleEqual" ], "⊵", [triangle]; + ["\\nltri"; "\\ntriangleleft"; "\\NotLeftTriangle" ], "⋪", [triangle]; + ["\\nrtri"; "\\ntriangleright"; "\\NotRightTriangle" ], "⋫", [triangle]; + ["\\nltrie"; "\\ntrianglelefteq"; "\\NotLeftTriangleEqual" ], "⋬", [triangle]; + ["\\nvltrie" ], "⋬̸", [triangle]; + ["\\nrtrie"; "\\ntrianglerighteq"; "\\NotRightTriangleEqual" ], "⋭", [triangle]; + ["\\nvrtrie" ], "⋭̸", [triangle]; + ["\\xutri"; "\\bigtriangleup" ], "△", [triangle]; + ["\\utrif"; "\\blacktriangle" ], "▴", [triangle]; + ["\\utri"; "\\triangle" ], "▵", [triangle]; + ["\\rtrif"; "\\blacktriangleright" ], "▸", [triangle]; + ["\\rtri"; "\\triangleright" ], "▹", [triangle]; + ["\\xdtri"; "\\bigtriangledown" ], "▽", [triangle]; + ["\\dtrif"; "\\blacktriangledown" ], "▾", [triangle]; + ["\\dtri"; "\\triangledown" ], "▿", [triangle]; + ["\\ltrif"; "\\blacktriangleleft" ], "◂", [triangle]; + ["\\ltri"; "\\triangleleft" ], "◃", [triangle]; + ["\\tridot" ], "◬", [triangle]; + ["\\ultri" ], "◸", [triangle]; + ["\\urtri" ], "◹", [triangle]; + ["\\lltri" ], "◺", [triangle]; + ["\\rtriltri" ], "⧎", [triangle]; + ["\\LeftTriangleBar" ], "⧏", [triangle]; + ["\\NotLeftTriangleBar" ], "⧏̸", [triangle]; + ["\\RightTriangleBar" ], "⧐", [triangle]; + ["\\NotRightTriangleBar" ], "⧐̸", [triangle]; +(* }}} *) + +(* {{{ arrows *) + ["\\larr"; "\\gets"; "\\leftarrow"; "\\LeftArrow";"\\<-" ], "←", [arrow]; + ["\\uarr"; "\\UpArrow"; "\\uparrow" ], "↑", [arrow]; + ["\\to"; "\\rarr"; "\\RightArrow"; "\\rightarrow";"\\->"], "→", [arrow]; + ["\\darr"; "\\downarrow"; "\\DownArrow" ], "↓", [arrow]; + ["\\harr"; "\\LeftRightArrow"; "\\leftrightarrow" ], "↔", [arrow]; + ["\\varr"; "\\updownarrow"; "\\UpDownArrow" ], "↕", [arrow]; + ["\\nwarr"; "\\nwarrow"; "\\UpperLeftArrow" ], "↖", [arrow]; + ["\\nearr"; "\\nearrow"; "\\UpperRightArrow" ], "↗", [arrow]; + ["\\searr"; "\\searrow"; "\\LowerRightArrow" ], "↘", [arrow]; + ["\\swarr"; "\\swarrow"; "\\LowerLeftArrow" ], "↙", [arrow]; + ["\\nlarr"; "\\nleftarrow" ], "↚", [arrow]; + ["\\nrarr"; "\\nrightarrow" ], "↛", [arrow]; + ["\\rarrw"; "\\rightsquigarrow" ], "↝", [arrow]; + ["\\nrarrw" ], "↝̸", [arrow]; + ["\\Larr"; "\\twoheadleftarrow" ], "↞", [arrow]; + ["\\Uarr" ], "↟", [arrow]; + ["\\Rarr"; "\\twoheadrightarrow" ], "↠", [arrow]; + ["\\Darr" ], "↡", [arrow]; + ["\\larrtl"; "\\leftarrowtail" ], "↢", [arrow]; + ["\\ratail"; "\\rarrtl"; "\\rightarrowtail" ], "↣", [arrow]; + ["\\mapstoleft"; "\\LeftTeeArrow" ], "↤", [arrow]; + ["\\mapstoup"; "\\UpTeeArrow" ], "↥", [arrow]; + ["\\map"; "\\mapsto"; "\\RightTeeArrow" ], "↦", [arrow]; + ["\\mapstodown"; "\\DownTeeArrow" ], "↧", [arrow]; + ["\\larrhk"; "\\hookleftarrow" ], "↩", [arrow]; + ["\\rarrhk"; "\\hookrightarrow" ], "↪", [arrow]; + ["\\larrlp"; "\\looparrowleft" ], "↫", [arrow]; + ["\\rarrlp"; "\\looparrowright" ], "↬", [arrow]; + ["\\harrw"; "\\leftrightsquigarrow" ], "↭", [arrow]; + ["\\nharr"; "\\nleftrightarrow" ], "↮", [arrow]; + ["\\Lsh"; "\\lsh" ], "↰", [arrow]; + ["\\Rsh"; "\\rsh" ], "↱", [arrow]; + ["\\ldsh" ], "↲", [arrow]; + ["\\rdsh" ], "↳", [arrow]; + ["\\cularr"; "\\curvearrowleft" ], "↶", [arrow]; + ["\\curarr"; "\\curvearrowright" ], "↷", [arrow]; + ["\\olarr"; "\\circlearrowleft" ], "↺", [arrow]; + ["\\orarr"; "\\circlearrowright" ], "↻", [arrow]; + ["\\lharu"; "\\LeftVector"; "\\leftharpoonup" ], "↼", [arrow]; + ["\\lhard"; "\\DownLeftVector"; "\\leftharpoondown" ], "↽", [arrow]; + ["\\uharr"; "\\RightUpVector"; "\\upharpoonright" ], "↾", [arrow]; + ["\\uharl"; "\\LeftUpVector"; "\\upharpoonleft" ], "↿", [arrow]; + ["\\rharu"; "\\RightVector"; "\\rightharpoonup" ], "⇀", [arrow]; + ["\\rhard"; "\\DownRightVector"; "\\rightharpoondown" ], "⇁", [arrow]; + ["\\dharr"; "\\RightDownVector"; "\\downharpoonright" ], "⇂", [arrow]; + ["\\dharl"; "\\LeftDownVector"; "\\downharpoonleft" ], "⇃", [arrow]; + ["\\rlarr"; "\\rightleftarrows"; "\\RightArrowLeftArrow" ], "⇄", [arrow]; + ["\\udarr"; "\\UpArrowDownArrow" ], "⇅", [arrow]; + ["\\lrarr"; "\\leftrightarrows"; "\\LeftArrowRightArrow" ], "⇆", [arrow]; + ["\\llarr"; "\\leftleftarrows" ], "⇇", [arrow]; + ["\\uuarr"; "\\upuparrows" ], "⇈", [arrow]; + ["\\rrarr"; "\\rightrightarrows" ], "⇉", [arrow]; + ["\\ddarr"; "\\downdownarrows" ], "⇊", [arrow]; + ["\\lrhar"; "\\leftrightharpoons"; "\\ReverseEquilibrium" ], "⇋", [arrow]; + ["\\rlhar"; "\\Equilibrium"; "\\rightleftharpoons" ], "⇌", [arrow]; + ["\\nlArr"; "\\nvlArr"; "\\nLeftarrow" ], "⇍", [arrow]; + ["\\nhArr"; "\\nvHarr"; "\\nLeftrightarrow" ], "⇎", [arrow]; + ["\\nrArr"; "\\nvrArr"; "\\nRightarrow" ], "⇏", [arrow]; + ["\\lArr"; "\\Leftarrow"; "\\DoubleLeftArrow";"\\<==" ], "⇐", [arrow]; + ["\\uArr"; "\\Uparrow"; "\\DoubleUpArrow" ], "⇑", [arrow]; + ["\\rArr"; "\\Implies"; "\\Rightarrow"; "\\Longrightarrow"; "\\DoubleRightArrow"; "\\==>"], "⇒", [arrow]; + ["\\dArr"; "\\Downarrow"; "\\DoubleDownArrow" ], "⇓", [arrow]; + ["\\iff"; "\\hArr"; "\\Leftrightarrow"; "\\DoubleLeftRightArrow";"\\<==>" ], "⇔", [arrow]; + ["\\vArr"; "\\Updownarrow"; "\\DoubleUpDownArrow" ], "⇕", [arrow]; + ["\\nwArr" ], "⇖", [arrow]; + ["\\neArr" ], "⇗", [arrow]; + ["\\seArr" ], "⇘", [arrow]; + ["\\swArr" ], "⇙", [arrow]; + ["\\lAarr"; "\\Lleftarrow" ], "⇚", [arrow]; + ["\\rAarr"; "\\Rrightarrow" ], "⇛", [arrow]; + ["\\zigrarr" ], "⇝", [arrow]; + ["\\larrb"; "\\LeftArrowBar" ], "⇤", [arrow]; + ["\\rarrb"; "\\RightArrowBar" ], "⇥", [arrow]; + ["\\duarr"; "\\DownArrowUpArrow" ], "⇵", [arrow]; + ["\\loarr" ], "⇽", [arrow]; + ["\\roarr" ], "⇾", [arrow]; + ["\\hoarr" ], "⇿", [arrow]; + ["\\Map" ], "⤅", [arrow]; + ["\\lbarr" ], "⤌", [arrow]; + ["\\rbarr"; "\\bkarow" ], "⤍", [arrow]; + ["\\lBarr" ], "⤎", [arrow]; + ["\\ac"; "\\rBarr"; "\\dbkarow" ], "⤏", [arrow]; + ["\\RBarr"; "\\drbkarow" ], "⤐", [arrow]; + ["\\DDotrahd" ], "⤑", [arrow]; + ["\\UpArrowBar" ], "⤒", [arrow]; + ["\\DownArrowBar" ], "⤓", [arrow]; + ["\\Rarrtl" ], "⤖", [arrow]; + ["\\latail" ], "⤙", [arrow]; + ["\\lAtail" ], "⤛", [arrow]; + ["\\rAtail" ], "⤜", [arrow]; + ["\\larrfs" ], "⤝", [arrow]; + ["\\rarrfs" ], "⤞", [arrow]; + ["\\larrbfs" ], "⤟", [arrow]; + ["\\rarrbfs" ], "⤠", [arrow]; + ["\\nwarhk" ], "⤣", [arrow]; + ["\\nearhk" ], "⤤", [arrow]; + ["\\searhk"; "\\hksearow" ], "⤥", [arrow]; + ["\\swarhk"; "\\hkswarow" ], "⤦", [arrow]; + ["\\nwnear" ], "⤧", [arrow]; + ["\\toea"; "\\nesear" ], "⤨", [arrow]; + ["\\tosa"; "\\seswar" ], "⤩", [arrow]; + ["\\swnwar" ], "⤪", [arrow]; + ["\\rarrc" ], "⤳", [arrow]; + ["\\nrarrc" ], "⤳̸", [arrow]; + ["\\cudarrr" ], "⤵", [arrow]; + ["\\ldca" ], "⤶", [arrow]; + ["\\rdca" ], "⤷", [arrow]; + ["\\cudarrl" ], "⤸", [arrow]; + ["\\larrpl" ], "⤹", [arrow]; + ["\\curarrm" ], "⤼", [arrow]; + ["\\cularrp" ], "⤽", [arrow]; + ["\\rarrpl" ], "⥅", [arrow]; + ["\\harrcir" ], "⥈", [arrow]; + ["\\Uarrocir" ], "⥉", [arrow]; + ["\\lurdshar" ], "⥊", [arrow]; + ["\\ldrushar" ], "⥋", [arrow]; + ["\\LeftRightVector" ], "⥎", [arrow]; + ["\\RightUpDownVector" ], "⥏", [arrow]; + ["\\DownLeftRightVector" ], "⥐", [arrow]; + ["\\LeftUpDownVector" ], "⥑", [arrow]; + ["\\LeftVectorBar" ], "⥒", [arrow]; + ["\\RightVectorBar" ], "⥓", [arrow]; + ["\\RightUpVectorBar" ], "⥔", [arrow]; + ["\\RightDownVectorBar" ], "⥕", [arrow]; + ["\\DownLeftVectorBar" ], "⥖", [arrow]; + ["\\DownRightVectorBar" ], "⥗", [arrow]; + ["\\LeftUpVectorBar" ], "⥘", [arrow]; + ["\\LeftDownVectorBar" ], "⥙", [arrow]; + ["\\LeftTeeVector" ], "⥚", [arrow]; + ["\\RightTeeVector" ], "⥛", [arrow]; + ["\\RightUpTeeVector" ], "⥜", [arrow]; + ["\\RightDownTeeVector" ], "⥝", [arrow]; + ["\\DownLeftTeeVector" ], "⥞", [arrow]; + ["\\DownRightTeeVector" ], "⥟", [arrow]; + ["\\LeftUpTeeVector" ], "⥠", [arrow]; + ["\\LeftDownTeeVector" ], "⥡", [arrow]; + ["\\lHar" ], "⥢", [arrow]; + ["\\uHar" ], "⥣", [arrow]; + ["\\rHar" ], "⥤", [arrow]; + ["\\dHar" ], "⥥", [arrow]; + ["\\luruhar" ], "⥦", [arrow]; + ["\\ldrdhar" ], "⥧", [arrow]; + ["\\ruluhar" ], "⥨", [arrow]; + ["\\rdldhar" ], "⥩", [arrow]; + ["\\lharul" ], "⥪", [arrow]; + ["\\llhard" ], "⥫", [arrow]; + ["\\rharul" ], "⥬", [arrow]; + ["\\lrhard" ], "⥭", [arrow]; + ["\\udhar"; "\\UpEquilibrium" ], "⥮", [arrow]; + ["\\duhar"; "\\ReverseUpEquilibrium" ], "⥯", [arrow]; + ["\\RoundImplies" ], "⥰", [arrow]; + ["\\erarr" ], "⥱", [arrow]; + ["\\simrarr" ], "⥲", [arrow]; + ["\\larrsim" ], "⥳", [arrow]; + ["\\rarrsim" ], "⥴", [arrow]; + ["\\rarrap" ], "⥵", [arrow]; + ["\\ltlarr" ], "⥶", [arrow]; + ["\\suplarr" ], "⥻", [arrow]; + ["\\lfisht" ], "⥼", [arrow]; + ["\\rfisht" ], "⥽", [arrow]; + ["\\ufisht" ], "⥾", [arrow]; + ["\\dfisht" ], "⥿", [arrow]; +(* }}} *) + +(* {{{ set operations *) + ["\\emptyv"; "\\varnothing" ], "∅", [set]; + ["\\in"; "\\isin"; "\\isinv"; "\\Element" ], "∈", [set]; + ["\\notin"; "\\NotElement" ], "∉", [set]; + ["\\notinva" ], "∉̸", [set]; + ["\\ni"; "\\niv"; "\\owns"; "\\SuchThat"; "\\ReverseElement" ], "∋", [set]; + ["\\notni"; "\\notniva"; "\\NotReverseElement" ], "∌", [set]; + ["\\coprod"; "\\Coproduct" ], "∐", [set]; + ["\\cap" ], "∩", [set]; + ["\\cup" ], "∪", [set]; + ["\\twixt"; "\\between" ], "≬", [set]; + ["\\subset" ], "⊂", [set]; + ["\\supset"; "\\Superset" ], "⊃", [set]; + ["\\suphsol" ], "⊃/", [set]; + ["\\nsub"; "\\vnsub"; "\\nsubset"; "\\NotSubset" ], "⊄", [set]; + ["\\nsup"; "\\vnsup"; "\\nsupset"; "\\NotSuperset" ], "⊅", [set]; + ["\\subE"; "\\sube"; "\\subseteq"; "\\subseteqq"; "\\SubsetEqual" ], "⊆", [set]; + ["\\supe"; "\\supE"; "\\supseteq"; "\\supseteqq"; "\\SupersetEqual"], "⊇", [set]; + ["\\nsube"; "\\nsubE"; "\\nsubseteq"; "\\nsubseteqq"; "\\NotSubsetEqual"], "⊈", [set]; + ["\\nsupe"; "\\nsupE"; "\\nsupseteq"; "\\nsupseteqq"; "\\NotSupersetEqual"], "⊉", [set]; + ["\\subne"; "\\subnE"; "\\subsetneq"; "\\subsetneqq" ], "⊊", [set]; + ["\\supne"; "\\supnE"; "\\supsetneq"; "\\supsetneqq" ], "⊋", [set]; + ["\\cupdot" ], "⊍", [set]; + ["\\uplus"; "\\xuplus"; "\\biguplus"; "\\UnionPlus" ], "⊎", [set]; + ["\\sqsub"; "\\sqsubset"; "\\SquareSubset" ], "⊏", [set]; + ["\\NotSquareSubset" ], "⊏̸", [set]; + ["\\sqsup"; "\\sqsupset"; "\\SquareSuperset" ], "⊐", [set]; + ["\\NotSquareSuperset" ], "⊐̸", [set]; + ["\\sqsube"; "\\sqsubseteq"; "\\SquareSubsetEqual" ], "⊑", [set]; + ["\\sqsupe"; "\\sqsupseteq"; "\\SquareSupersetEqual" ], "⊒", [set]; + ["\\sqcap"; "\\SquareIntersection" ], "⊓", [set]; + ["\\sqcup"; "\\xsqcup"; "\\bigsqcup"; "\\SquareUnion" ], "⊔", [set]; + ["\\xcap"; "\\bigcap"; "\\Intersection" ], "⋂", [set]; + ["\\xcup"; "\\Union"; "\\bigcup" ], "⋃", [set]; + ["\\Sub"; "\\Subset" ], "⋐", [set]; + ["\\Sup"; "\\Supset" ], "⋑", [set]; + ["\\Cap" ], "⋒", [set]; + ["\\Cup" ], "⋓", [set]; + ["\\nsqsube"; "\\NotSquareSubsetEqual" ], "⋢", [set]; + ["\\nsqsupe"; "\\NotSquareSupersetEqual" ], "⋣", [set]; + ["\\disin" ], "⋲", [set]; + ["\\isinsv" ], "⋳", [set]; + ["\\isins" ], "⋴", [set]; + ["\\isindot" ], "⋵", [set]; + ["\\notinvc" ], "⋶", [set]; + ["\\notindot" ], "⋶︀", [set]; + ["\\notinvb" ], "⋷", [set]; + ["\\isinE" ], "⋹", [set]; + ["\\nisd" ], "⋺", [set]; + ["\\xnis" ], "⋻", [set]; + ["\\nis" ], "⋼", [set]; + ["\\notnivc" ], "⋽", [set]; + ["\\notnivb" ], "⋾", [set]; + ["\\subrarr" ], "⥹", [set]; +(* }}} *) + +(* {{{ math *) + ["\\pm"; "\\plusmn"; "\\PlusMinus" ], "±", [math]; + ["\\times" ], "×", [math]; + ["\\div"; "\\divide" ], "÷", [math]; + ["\\prod"; "\\Product" ], "∏", [math]; + ["\\sum"; "\\Sum" ], "∑", [math]; + ["\\mp"; "\\mnplus"; "\\MinusPlus" ], "∓", [math]; + ["\\plusdo"; "\\dotplus" ], "∔", [math]; + ["\\setmn"; "\\setminus"; "\\Backslash" ], "∖", [math]; + ["\\lowast" ], "∗", [math]; + ["\\Sqrt"; "\\radic" ], "√", [math]; + ["\\prop"; "\\vprop"; "\\propto"; "\\varpropto"; "\\Proportional" ], "∝", [math]; + ["\\infty"; "\\infin" ], "∞", [math]; + ["\\mid"; "\\divides"; "\\VerticalBar" ], "∣", [math]; + ["\\nmid"; "\\ndivides"; "\\NotVerticalBar" ], "∤", [math]; + ["\\npar"; "\\nparallel"; "\\NotDoubleVerticalBar" ], "∦", [math]; + ["\\int"; "\\Integral" ], "∫", [math]; + ["\\Int" ], "∬", [math]; + ["\\tint"; "\\iiint" ], "∭", [math]; + ["\\oint"; "\\conint"; "\\ContourIntegral" ], "∮", [math]; + ["\\Conint"; "\\DoubleContourIntegral" ], "∯", [math]; + ["\\Cconint" ], "∰", [math]; + ["\\cwint" ], "∱", [math]; + ["\\cwconint"; "\\ClockwiseContourIntegral" ], "∲", [math]; + ["\\awconint"; "\\CounterClockwiseContourIntegral" ], "∳", [math]; + ["\\qint"; "\\iiiint" ], "⨌", [math]; + ["\\cirfnint" ], "⨐", [math]; + ["\\awint" ], "⨑", [math]; + ["\\rppolint" ], "⨒", [math]; + ["\\scpolint" ], "⨓", [math]; + ["\\npolint" ], "⨔", [math]; + ["\\pointint" ], "⨕", [math]; + ["\\quatint" ], "⨖", [math]; + ["\\intlarhk" ], "⨗", [math]; + ["\\Cross" ], "⨯", [math]; +(* }}} *) + +(* {{{ spaces *) + ["\\nbsp"; "\\NonBreakingSpace" ], " ", [space]; + ["\\shy" ], "­", [space]; + ["\\ensp" ], " ", [space]; + ["\\emsp" ], " ", [space]; + ["\\emsp13" ], " ", [space]; + ["\\emsp14" ], " ", [space]; + ["\\numsp" ], " ", [space]; + ["\\puncsp" ], " ", [space]; + ["\\thinsp"; "\\ThinSpace" ], " ", [space]; + ["\\ThickSpace" ], "   ", [space]; + ["\\hairsp"; "\\VeryThinSpace" ], " ", [space]; + ["\\ic"; "\\ZeroWidthSpace"; "\\InvisibleComma" ], "​", [space]; + ["\\af"; "\\ApplyFunction" ], "⁡", [space]; + ["\\it"; "\\InvisibleTimes" ], "⁢", [space]; + ["\\NoBreak" ], "", [space]; +(* }}} *) + +(* {{{ parenteses *) + ["\\laquo" ], "«", [delimiter] ; + ["\\raquo" ], "»", [delimiter] ; + ["\\lang"; "\\langle"; "\\LeftAngleBracket" ], "〈", [delimiter] ; + ["\\rang"; "\\rangle"; "\\RightAngleBracket" ], "〉", [delimiter] ; + ["\\lmoust"; "\\lmoustache" ], "⎰", [delimiter] ; + ["\\rmoust"; "\\rmoustache" ], "⎱", [delimiter] ; + ["\\Lang" ], "《", [delimiter] ; + ["\\Rang" ], "》", [delimiter] ; + ["\\lbbrk" ], "〔", [delimiter] ; + ["\\rbbrk" ], "〕", [delimiter] ; + ["\\lopar" ], "〘", [delimiter] ; + ["\\ropar" ], "〙", [delimiter] ; + ["\\lobrk"; "\\LeftDoubleBracket" ], "〚", [delimiter] ; + ["\\robrk"; "\\RightDoubleBracket" ], "〛", [delimiter] ; +(* }}} *) + +(* {{{ 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]; + ["\\bnequiv" ], "≡⃥", [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]; + ["\\prurel" ], "⊰", [miscellanea]; + ["\\lesg" ], "⋚︀", [miscellanea]; + ["\\gesl" ], "⋛︀", [miscellanea]; + ["\\ShortUpArrow" ], "⌃︀", [miscellanea]; + ["\\ShortDownArrow" ], "⌄︀", [miscellanea]; + ["\\target" ], "⌖", [miscellanea]; + ["\\cylcty" ], "⌭", [miscellanea]; + ["\\profalar" ], "⌮", [miscellanea]; + ["\\topbot" ], "⌶", [miscellanea]; + ["\\solbar" ], "⌿", [miscellanea]; + ["\\angzarr" ], "⍼", [miscellanea]; + ["\\tbrk"; "\\OverBracket" ], "⎴", [miscellanea]; + ["\\bbrk"; "\\UnderBracket" ], "⎵", [miscellanea]; + ["\\lbrke" ], "⦋", [miscellanea]; + ["\\rbrke" ], "⦌", [miscellanea]; + ["\\lbrkslu" ], "⦍", [miscellanea]; + ["\\rbrksld" ], "⦎", [miscellanea]; + ["\\lbrksld" ], "⦏", [miscellanea]; + ["\\rbrkslu" ], "⦐", [miscellanea]; + ["\\langd" ], "⦑", [miscellanea]; + ["\\rangd" ], "⦒", [miscellanea]; + ["\\lparlt" ], "⦓", [miscellanea]; + ["\\rpargt" ], "⦔", [miscellanea]; + ["\\gtlPar" ], "⦕", [miscellanea]; + ["\\ltrPar" ], "⦖", [miscellanea]; + ["\\vzigzag" ], "⦚", [miscellanea]; + ["\\angrtvbd" ], "⦝", [miscellanea]; + ["\\angrtvb" ], "⦝︀", [miscellanea]; + ["\\ange" ], "⦤", [miscellanea]; + ["\\range" ], "⦥", [miscellanea]; + ["\\dwangle" ], "⦦", [miscellanea]; + ["\\uwangle" ], "⦧", [miscellanea]; + ["\\angmsdaa" ], "⦨", [miscellanea]; + ["\\angmsdab" ], "⦩", [miscellanea]; + ["\\angmsdac" ], "⦪", [miscellanea]; + ["\\angmsdad" ], "⦫", [miscellanea]; + ["\\angmsdae" ], "⦬", [miscellanea]; + ["\\angmsdaf" ], "⦭", [miscellanea]; + ["\\angmsdag" ], "⦮", [miscellanea]; + ["\\angmsdah" ], "⦯", [miscellanea]; + ["\\bemptyv" ], "⦰", [miscellanea]; + ["\\demptyv" ], "⦱", [miscellanea]; + ["\\cemptyv" ], "⦲", [miscellanea]; + ["\\raemptyv" ], "⦳", [miscellanea]; + ["\\laemptyv" ], "⦴", [miscellanea]; + ["\\ohbar" ], "⦵", [miscellanea]; + ["\\omid" ], "⦶", [miscellanea]; + ["\\opar" ], "⦷", [miscellanea]; + ["\\operp" ], "⦹", [miscellanea]; + ["\\olcross" ], "⦻", [miscellanea]; + ["\\odsold" ], "⦼", [miscellanea]; + ["\\olcir" ], "⦾", [miscellanea]; + ["\\ofcir" ], "⦿", [miscellanea]; + ["\\olt" ], "⧀", [miscellanea]; + ["\\ogt" ], "⧁", [miscellanea]; + ["\\cirscir" ], "⧂", [miscellanea]; + ["\\cirE" ], "⧃", [miscellanea]; + ["\\solb" ], "⧄", [miscellanea]; + ["\\bsolb" ], "⧅", [miscellanea]; + ["\\boxbox" ], "⧉", [miscellanea]; + ["\\trisb" ], "⧍", [miscellanea]; + ["\\race" ], "⧚", [miscellanea]; + ["\\acE" ], "⧛", [miscellanea]; + ["\\iinfin" ], "⧜", [miscellanea]; + ["\\nvinfin" ], "⧞", [miscellanea]; + ["\\eparsl" ], "⧣", [miscellanea]; + ["\\smeparsl" ], "⧤", [miscellanea]; + ["\\eqvparsl" ], "⧥", [miscellanea]; + ["\\RuleDelayed" ], "⧴", [miscellanea]; + ["\\dsol" ], "⧶", [miscellanea]; + ["\\pluscir" ], "⨢", [miscellanea]; + ["\\plusacir" ], "⨣", [miscellanea]; + ["\\simplus" ], "⨤", [miscellanea]; + ["\\plusdu" ], "⨥", [miscellanea]; + ["\\plussim" ], "⨦", [miscellanea]; + ["\\plustwo" ], "⨧", [miscellanea]; + ["\\mcomma" ], "⨩", [miscellanea]; + ["\\minusdu" ], "⨪", [miscellanea]; + ["\\loplus" ], "⨭", [miscellanea]; + ["\\roplus" ], "⨮", [miscellanea]; + ["\\timesd" ], "⨰", [miscellanea]; + ["\\timesbar" ], "⨱", [miscellanea]; + ["\\smashp" ], "⨳", [miscellanea]; + ["\\lotimes" ], "⨴", [miscellanea]; + ["\\rotimes" ], "⨵", [miscellanea]; + ["\\otimesas" ], "⨶", [miscellanea]; + ["\\Otimes" ], "⨷", [miscellanea]; + ["\\odiv" ], "⨸", [miscellanea]; + ["\\triplus" ], "⨹", [miscellanea]; + ["\\triminus" ], "⨺", [miscellanea]; + ["\\tritime" ], "⨻", [miscellanea]; + ["\\iprod"; "\\intprod" ], "⨼", [miscellanea]; + ["\\amalg" ], "⨿", [miscellanea]; + ["\\capdot" ], "⩀", [miscellanea]; + ["\\ncup" ], "⩂", [miscellanea]; + ["\\ncap" ], "⩃", [miscellanea]; + ["\\capand" ], "⩄", [miscellanea]; + ["\\cupor" ], "⩅", [miscellanea]; + ["\\cupcap" ], "⩆", [miscellanea]; + ["\\capcup" ], "⩇", [miscellanea]; + ["\\cupbrcap" ], "⩈", [miscellanea]; + ["\\capbrcup" ], "⩉", [miscellanea]; + ["\\cupcup" ], "⩊", [miscellanea]; + ["\\capcap" ], "⩋", [miscellanea]; + ["\\ccups" ], "⩌", [miscellanea]; + ["\\ccaps" ], "⩍", [miscellanea]; + ["\\ccupssm" ], "⩐", [miscellanea]; + ["\\And" ], "⩓", [miscellanea]; + ["\\Or" ], "⩔", [miscellanea]; + ["\\andand" ], "⩕", [miscellanea]; + ["\\oror" ], "⩖", [miscellanea]; + ["\\orslope" ], "⩗", [miscellanea]; + ["\\andslope" ], "⩘", [miscellanea]; + ["\\andv" ], "⩚", [miscellanea]; + ["\\orv" ], "⩛", [miscellanea]; + ["\\andd" ], "⩜", [miscellanea]; + ["\\ord" ], "⩝", [miscellanea]; + ["\\wedbar" ], "⩟", [miscellanea]; + ["\\sdote" ], "⩦", [miscellanea]; + ["\\simdot" ], "⩪", [miscellanea]; + ["\\congdot" ], "⩭", [miscellanea]; + ["\\ncongdot" ], "⩭̸", [miscellanea]; + ["\\apacir" ], "⩯", [miscellanea]; + ["\\napE" ], "⩰̸", [miscellanea]; + ["\\eplus" ], "⩱", [miscellanea]; + ["\\pluse" ], "⩲", [miscellanea]; + ["\\Esim" ], "⩳", [miscellanea]; + ["\\Colone" ], "⩴", [miscellanea]; + ["\\Equal" ], "⩵", [miscellanea]; + ["\\eDDot"; "\\ddotseq" ], "⩷", [miscellanea]; + ["\\equivDD" ], "⩸", [miscellanea]; + ["\\ltcir" ], "⩹", [miscellanea]; + ["\\gtcir" ], "⩺", [miscellanea]; + ["\\ltquest" ], "⩻", [miscellanea]; + ["\\gtquest" ], "⩼", [miscellanea]; + ["\\LessLess" ], "⪡", [miscellanea]; + ["\\GreaterGreater" ], "⪢", [miscellanea]; + ["\\glj" ], "⪤", [miscellanea]; + ["\\gla" ], "⪥", [miscellanea]; + ["\\ltcc" ], "⪦", [miscellanea]; + ["\\gtcc" ], "⪧", [miscellanea]; + ["\\lescc" ], "⪨", [miscellanea]; + ["\\gescc" ], "⪩", [miscellanea]; + ["\\smt" ], "⪪", [miscellanea]; + ["\\lat" ], "⪫", [miscellanea]; + ["\\smte" ], "⪬", [miscellanea]; + ["\\smtes" ], "⪬︀", [miscellanea]; + ["\\late" ], "⪭", [miscellanea]; + ["\\lates" ], "⪭︀", [miscellanea]; + ["\\Sc" ], "⪼", [miscellanea]; + ["\\subdot" ], "⪽", [miscellanea]; + ["\\supdot" ], "⪾", [miscellanea]; + ["\\subplus" ], "⪿", [miscellanea]; + ["\\supplus" ], "⫀", [miscellanea]; + ["\\submult" ], "⫁", [miscellanea]; + ["\\supmult" ], "⫂", [miscellanea]; + ["\\subedot" ], "⫃", [miscellanea]; + ["\\supedot" ], "⫄", [miscellanea]; + ["\\subsim" ], "⫇", [miscellanea]; + ["\\supsim" ], "⫈", [miscellanea]; + ["\\csub" ], "⫏", [miscellanea]; + ["\\csup" ], "⫐", [miscellanea]; + ["\\csube" ], "⫑", [miscellanea]; + ["\\csupe" ], "⫒", [miscellanea]; + ["\\subsup" ], "⫓", [miscellanea]; + ["\\supsub" ], "⫔", [miscellanea]; + ["\\subsub" ], "⫕", [miscellanea]; + ["\\supsup" ], "⫖", [miscellanea]; + ["\\suphsub" ], "⫗", [miscellanea]; + ["\\supdsub" ], "⫘", [miscellanea]; + ["\\forkv" ], "⫙", [miscellanea]; + ["\\topfork" ], "⫚", [miscellanea]; + ["\\mlcp" ], "⫛", [miscellanea]; + ["\\Dashv"; "\\DoubleLeftTee" ], "⫤", [miscellanea]; + ["\\Vdashl" ], "⫦", [miscellanea]; + ["\\Barv" ], "⫧", [miscellanea]; + ["\\vBar" ], "⫨", [miscellanea]; + ["\\vBarv" ], "⫩", [miscellanea]; + ["\\Vbar" ], "⫫", [miscellanea]; + ["\\Not" ], "⫬", [miscellanea]; + ["\\bNot" ], "⫭", [miscellanea]; + ["\\rnmid" ], "⫮", [miscellanea]; + ["\\cirmid" ], "⫯", [miscellanea]; + ["\\midcir" ], "⫰", [miscellanea]; + ["\\topcir" ], "⫱", [miscellanea]; + ["\\nhpar" ], "⫲", [miscellanea]; + ["\\parsim" ], "⫳", [miscellanea]; + ["\\loang" ], "", [miscellanea]; + ["\\roang" ], "", [miscellanea]; + ["\\xlarr"; "\\LongLeftArrow" ], "", [miscellanea]; + ["\\xrarr"; "\\LongRightArrow" ], "", [miscellanea]; + ["\\xharr"; "\\LongLeftRightArrow" ], "", [miscellanea]; + ["\\xlArr"; "\\DoubleLongLeftArrow" ], "", [miscellanea]; + ["\\xrArr"; "\\DoubleLongRightArrow" ], "", [miscellanea]; + ["\\xhArr"; "\\DoubleLongLeftRightArrow" ], "", [miscellanea]; + ["\\xmap" ], "", [miscellanea]; + ["\\FilledVerySmallSquare" ], "", [miscellanea]; + ["\\EmptyVerySmallSquare" ], "", [miscellanea]; + ["\\dzigrarr" ], "", [miscellanea]; + ["\\Ascr" ], "𝒜", [miscellanea]; + ["\\Cscr" ], "𝒞", [miscellanea]; + ["\\Dscr" ], "𝒟", [miscellanea]; + ["\\Gscr" ], "𝒢", [miscellanea]; + ["\\Jscr" ], "𝒥", [miscellanea]; + ["\\Kscr" ], "𝒦", [miscellanea]; + ["\\Nscr" ], "𝒩", [miscellanea]; + ["\\Oscr" ], "𝒪", [miscellanea]; + ["\\Pscr" ], "𝒫", [miscellanea]; + ["\\Qscr" ], "𝒬", [miscellanea]; + ["\\Sscr" ], "𝒮", [miscellanea]; + ["\\Tscr" ], "𝒯", [miscellanea]; + ["\\Uscr" ], "𝒰", [miscellanea]; + ["\\Vscr" ], "𝒱", [miscellanea]; + ["\\Wscr" ], "𝒲", [miscellanea]; + ["\\Xscr" ], "𝒳", [miscellanea]; + ["\\Yscr" ], "𝒴", [miscellanea]; + ["\\Zscr" ], "𝒵", [miscellanea]; + ["\\ascr" ], "𝒶", [miscellanea]; + ["\\bscr" ], "𝒷", [miscellanea]; + ["\\cscr" ], "𝒸", [miscellanea]; + ["\\dscr" ], "𝒹", [miscellanea]; + ["\\fscr" ], "𝒻", [miscellanea]; + ["\\hscr" ], "𝒽", [miscellanea]; + ["\\iscr" ], "𝒾", [miscellanea]; + ["\\jscr" ], "𝒿", [miscellanea]; + ["\\kscr" ], "𝓀", [miscellanea]; + ["\\mscr" ], "𝓂", [miscellanea]; + ["\\nscr" ], "𝓃", [miscellanea]; + ["\\pscr" ], "𝓅", [miscellanea]; + ["\\qscr" ], "𝓆", [miscellanea]; + ["\\rscr" ], "𝓇", [miscellanea]; + ["\\sscr" ], "𝓈", [miscellanea]; + ["\\tscr" ], "𝓉", [miscellanea]; + ["\\uscr" ], "𝓊", [miscellanea]; + ["\\vscr" ], "𝓋", [miscellanea]; + ["\\wscr" ], "𝓌", [miscellanea]; + ["\\xscr" ], "𝓍", [miscellanea]; + ["\\yscr" ], "𝓎", [miscellanea]; + ["\\zscr" ], "𝓏", [miscellanea]; + ["\\Afr" ], "𝔄", [miscellanea]; + ["\\Bfr" ], "𝔅", [miscellanea]; + ["\\Dfr" ], "𝔇", [miscellanea]; + ["\\Efr" ], "𝔈", [miscellanea]; + ["\\Ffr" ], "𝔉", [miscellanea]; + ["\\Gfr" ], "𝔊", [miscellanea]; + ["\\Jfr" ], "𝔍", [miscellanea]; + ["\\Kfr" ], "𝔎", [miscellanea]; + ["\\Lfr" ], "𝔏", [miscellanea]; + ["\\Mfr" ], "𝔐", [miscellanea]; + ["\\Nfr" ], "𝔑", [miscellanea]; + ["\\Ofr" ], "𝔒", [miscellanea]; + ["\\Pfr" ], "𝔓", [miscellanea]; + ["\\Qfr" ], "𝔔", [miscellanea]; + ["\\Sfr" ], "𝔖", [miscellanea]; + ["\\Tfr" ], "𝔗", [miscellanea]; + ["\\Ufr" ], "𝔘", [miscellanea]; + ["\\Vfr" ], "𝔙", [miscellanea]; + ["\\Wfr" ], "𝔚", [miscellanea]; + ["\\Xfr" ], "𝔛", [miscellanea]; + ["\\Yfr" ], "𝔜", [miscellanea]; + ["\\afr" ], "𝔞", [miscellanea]; + ["\\bfr" ], "𝔟", [miscellanea]; + ["\\cfr" ], "𝔠", [miscellanea]; + ["\\dfr" ], "𝔡", [miscellanea]; + ["\\efr" ], "𝔢", [miscellanea]; + ["\\ffr" ], "𝔣", [miscellanea]; + ["\\gfr" ], "𝔤", [miscellanea]; + ["\\hfr" ], "𝔥", [miscellanea]; + ["\\ifr" ], "𝔦", [miscellanea]; + ["\\jfr" ], "𝔧", [miscellanea]; + ["\\kfr" ], "𝔨", [miscellanea]; + ["\\lfr" ], "𝔩", [miscellanea]; + ["\\mfr" ], "𝔪", [miscellanea]; + ["\\nfr" ], "𝔫", [miscellanea]; + ["\\ofr" ], "𝔬", [miscellanea]; + ["\\pfr" ], "𝔭", [miscellanea]; + ["\\qfr" ], "𝔮", [miscellanea]; + ["\\rfr" ], "𝔯", [miscellanea]; + ["\\sfr" ], "𝔰", [miscellanea]; + ["\\tfr" ], "𝔱", [miscellanea]; + ["\\ufr" ], "𝔲", [miscellanea]; + ["\\vfr" ], "𝔳", [miscellanea]; + ["\\wfr" ], "𝔴", [miscellanea]; + ["\\xfr" ], "𝔵", [miscellanea]; + ["\\yfr" ], "𝔶", [miscellanea]; + ["\\zfr" ], "𝔷", [miscellanea]; +(* }}} *) + +] + + +(** **************************************************************************) +(** * Bindings set 2 *) + +let bindings_set_2 = [ + + (** Symbols *) + "\\!'", "¡"; + "\\`", "‘"; + "\\``", "“"; + "\\'", "′"; + "\\''", "″"; + "\\'''", "‴"; + "\\mbox''", "”"; + "\\mbox'", "’"; + "\\--", "–"; + "\\---", "—"; + "\\Alpha", "Α"; + "\\Beta", "Β"; + "\\Box", "□"; + "\\Bumpeq", "≎"; + "\\Cap", "⋒"; + "\\Chi", "Χ"; + "\\Cup", "⋓"; + "\\DH", "Ð"; + "\\Delta", "Δ "; + "\\Diamond", "◇"; + "\\Downarrow", "⇓"; + "\\Epsilon", "Ε "; + "\\Eta", "Η"; + "\\Finv", "Ⅎ"; + "\\Gamma", "Γ "; + "\\Im", "ℑ"; + "\\Join", "⋈"; + "\\Kappa", "Κ"; + "\\L", "Ł"; + "\\Lambda", "Λ"; + "\\Leftarrow", "⇐"; + "\\Leftrightarrow", "⇔"; + "\\Lleftarrow", "⇚"; + "\\Longleftarrow", "⇐"; + "\\Longleftrightarrow", "⇔"; + "\\Longrightarrow", "⇒"; + "\\Lsh", "↰"; + "\\Mu", "Μ"; + "\\Nu", "Ν"; + "\\O", "Ø"; + "\\OE", "Œ"; + "\\Omega", "Ω"; + "\\W", "Ω"; + "\\Omicron", "Ο"; + "\\P", "¶"; + "\\Phi", "Φ"; + "\\F", "Φ"; + "\\Pi", "Π"; + "\\Psi", "Ψ"; + "\\Re", "ℜ"; + "\\Rho", "Ρ"; + "\\Rightarrow", "⇒"; + "\\Rrightarrow", "⇛"; + "\\Rsh", "↱"; + "\\S", "§"; + "\\Sigma", "Σ"; + "\\Subset", "⋐"; + "\\Supset", "⋑"; + "\\TH", "Þ"; + "\\Tau", "Τ"; + "\\Theta", "Θ"; + "\\Uparrow", "⇑"; + "\\Updownarrow", "⇕"; + "\\Upsilon", "Υ"; + "\\Vdash", "⊩"; + "\\Vvdash", "⊪"; + "\\Xi", "Ξ"; + "\\Zeta", "Ζ"; + "\\aa", "å"; + "\\ae", "æ"; + "\\aleph", "ℵ"; + "\\alpha", "α"; + "\\angle", "∠"; + "\\approx", "≈"; + "\\approxeq", "≊"; + "\\aquarius", "♒"; + "\\aries", "♈"; + "\\ascnode", "☊"; + "\\ast", "∗"; + "\\astrosun", "☉"; + "\\asymp", "≍"; + "\\backepsilon", "∍"; + "\\backprime", "‵"; + "\\backsim", "∽"; + "\\barwedge", "⊼"; + "\\because", "∵"; + "\\beta", "β"; + "\\beth", "ℶ"; + "\\between", "≬"; + "\\bigcap", "⋂"; + "\\bigcirc", "○"; + "\\bigcup", "⋃"; + "\\bigodot", "⊙"; + "\\bigoplus", "⊕"; + "\\bigotimes", "⊗"; + "\\bigsqcup", "⊔"; + "\\bigstar", "★"; + "\\bigtriangledown", "▽"; + "\\bigtriangleup", "△"; + "\\biguplus", "⊎"; + "\\bigvee", "⋁"; + "\\bigwedge", "⋀"; + "\\blackbishop", "♝"; + "\\blackking", "♚"; + "\\blackknight", "♞"; + "\\blacklozenge", "◆"; + "\\blackpawn", "♟"; + "\\blackqueen", "♛"; + "\\blackrook", "♜"; + "\\blacksquare", "■"; + "\\blacktriangle", "▲"; + "\\blacktriangledown", "▼"; + "\\blacktriangleleft", "◀"; + "\\blacktriangleright", "▷"; + "\\bot", "⊥"; + "\\bowtie", "⋈"; + "\\boxdot", "⊡"; + "\\boxminus", "⊟"; + "\\boxplus", "⊞"; + "\\boxtimes", "⊠"; + "\\bullet", "∙"; + "\\bumpeq", "≏"; + "\\cancer", "♋"; + "\\cap", "∩"; + "\\capricornus", "♑"; + "\\capslockkey", "⇪"; + "\\cdot", "⋅"; + "\\cdots", "⋯"; + "\\centerdot", "⋅"; + "\\cents", "¢"; + "\\chi", "χ"; + "\\circ", "∘"; + "\\circeq", "≗"; + "\\circlearrowleft", "↺"; + "\\circlearrowright", "↻"; + "\\circledS", "Ⓢ"; + "\\circledast", "⊛"; + "\\circledcirc", "⊚"; + "\\circleddash", "⊝"; + "\\clubsuit", "♣"; + "\\cmdkey", "⌘"; + "\\complement", "∁"; + "\\cong", "≅"; + "\\conjunction", "☌"; + "\\coprod", "∐"; + "\\copyright", "©"; + "\\cup", "∪"; + "\\curlyeqprec", "⋞"; + "\\curlyeqsucc", "⋟"; + "\\curlyvee", "⋎"; + "\\curlywedge", "⋏"; + "\\curvearrowleft", "↶"; + "\\curvearrowright", "↷"; + "\\cC", "Ç"; + "\\cc", "ç"; + "\\dag", "†"; + "\\dagger", "†"; + "\\daleth", "ℸ"; + "\\dashleftarrow", "⇠"; + "\\dashrightarrow", "⇢"; + "\\dashv", "⊣"; + "\\ddag", "‡"; + "\\ddagger", "‡"; + "\\degree", "°"; + "\\delkey", "⌫"; + "\\delta", "δ "; + "\\descnode", "☋"; + "\\dh", "ð"; + "\\diamond", "⋄"; + "\\diamondsuit", "♢"; + "\\digamma", "Ϝ"; + "\\div", "÷"; + "\\divideontimes", "⋇"; + "\\downarrow", "↓"; + "\\downdownarrows", "⇊"; + "\\downharpoonleft", "⇃"; + "\\downharpoonright", "⇂"; + "\\earth", "⊕"; + "\\ejectkey", "⏏"; + "\\ell", "ℓ"; + "\\emptyset", "∅"; + "\\enterkey", "⌤"; + "\\epsdice1", "⚀"; + "\\epsdice2", "⚁"; + "\\epsdice3", "⚂"; + "\\epsdice4", "⚃"; + "\\epsdice5", "⚄"; + "\\epsdice6", "⚅"; + "\\epsilon", "∊"; + "\\eqcirc", "≖"; + "\\equiv", "≡"; + "\\esckey", "⎋"; + "\\eta", "η"; + "\\eth", "ð"; + "\\euro", "€"; + "\\exists", "∃"; + "\\fallingdotseq", "≒"; + "\\flat", "♭"; + "\\forall", "∀"; + "\\frown", "⌢"; + "\\gamma", "γ"; + "\\ge", "≥"; + "\\gemini", "♊"; + "\\geq", "≥"; + "\\geqq", "≧"; + "\\gg", "≫"; + "\\ggg", "⋙"; + "\\gimel", "ℷ"; + "\\gtrdot", "⋗"; + "\\gtreqless", "⋛"; + "\\gtrless", "≷"; + "\\gtrsim", "≳"; + "\\hbar", "ℏ"; + "\\heartsuit", "♡"; + "\\hookleftarrow", "↩"; + "\\hookrightarrow", "↪"; + "\\hslash", "ℏ"; + "\\iiiint", "⨌"; + "\\iiint", "∭"; + "\\iint", "∬"; + "\\implies", "⇒"; + "\\in", "∈"; + "\\infty", "∞"; + "\\int", "∫"; + "\\intercal", "⊺"; + "\\iota", "ι"; + "\\jupiter", "♃"; + "\\kappa", "κ"; + "\\l{}", "ł"; + "\\lambda", "λ"; + "\\langle", "⟨"; + "\\lceil", "⌈"; + "\\ldots", "…"; + "\\le", "≤"; + "\\leadsto", "↝"; + "\\leftarrow", "←"; + "\\leftarrowtail", "↢"; + "\\leftharpoondown", "↽"; + "\\leftharpoonup", "↼"; + "\\leftleftarrows", "⇇"; + "\\leftmoon", "☾"; + "\\leftrightarrow", "↔"; + "\\leftrightarrows", "⇆"; + "\\leftrightharpoons", "⇋"; + "\\leftrightsquigarrow", "↭"; + "\\leftthreetimes", "⋋"; + "\\leo", "♌"; + "\\leq", "≤"; + "\\leqq", "≦"; + "\\leqslant", "≤"; + "\\lessdot", "⋖"; + "\\lesseqgtr", "⋚"; + "\\lessgtr", "≶"; + "\\lesssim", "≲"; + "\\lfloor", "⌊"; + "\\lhd", "⊲"; + "\\libra", "♎"; + "\\ll", "≪"; + "\\lll", "⋘"; + "\\longleftarrow", "←"; + "\\longleftrightarrow", "↔"; + "\\longmapsto", "⇖"; + "\\longrightarrow", "→"; + "\\looparrowleft", "↫"; + "\\looparrowright", "↬"; + "\\lozenge", "◊"; + "\\ltimes", "⋉"; + "\\mapsto", "↦"; + "\\mars", "♂"; + "\\measuredangle", "∡"; + "\\mercury", "☿"; + "\\mho", "℧"; + "\\mid", "∣"; + "\\models", "⊨"; + "\\mp", "∓"; + "\\mu", "μ"; + "\\multimap", "⊸"; + "\\nabla", "∇"; + "\\natural", "♮"; + "\\nearrow", "↗"; + "\\neg", "¬"; + "\\neptune", "♆"; + "\\neq", "≠"; + "\\nexists", "∄"; + "\\ng", "ŋ"; + "\\ni", "∋"; + "\\not<", "≮"; + "\\not>", "≯"; + "\\not\\Vdash", "⊮"; + "\\not\\approx", "≉"; + "\\not\\cong", "≇"; + "\\not\\equiv", "≢"; + "\\not\\ge", "≱"; + "\\not\\gtrless", "≹"; + "\\not\\in", "∉"; + "\\not\\le", "≰"; + "\\not\\models", "⊭"; + "\\not\\ni", "∌"; + "\\not\\sim", "≄"; + "\\not\\sqsubseteq", "⋢"; + "\\not\\sqsupseteq", "⋣"; + "\\not\\subset", "⊄"; + "\\not\\subseteq", "⊈"; + "\\not\\supset", "⊅"; + "\\not\\supseteq", "⊉"; + "\\not\\vdash", "⊬"; + "\\notin", "∉"; + "\\nu", "ν"; + "\\v", "ν"; + "\\nwarrow", "↖"; + "\\o{}", "ø"; + "\\odot", "⊙"; + "\\oe", "œ"; + "\\oint", "∮"; + "\\omega", "ω"; + "\\w", "ω"; + "\\omicron", "ο"; + "\\ominus", "⊖"; + "\\oplus", "⊕"; + "\\opposition", "☍"; + "\\optkey", "⌥"; + "\\oslash", "⊘"; + "\\otimes", "⊗"; + "\\parallel", "∥"; + "\\partial", "∂"; + "\\perp", "⊥"; + "\\phi", "φ"; + "\\f", "φ"; + "\\pi", "π"; + "\\pilcrow", "¶"; + "\\pisces", "♓"; + "\\pitchfork", "⋔"; + "\\pluto", "♇"; + "\\pm", "±"; + "\\pound", "£"; + "\\pounds", "£"; + "\\prec", "≺"; + "\\preccurlyeq", "≼"; + "\\preceq", "≼"; + "\\precsim", "≾"; + "\\prime", "′"; + "\\prod", "∏"; + "\\propto", "∝"; + "\\psi", "ψ"; + "\\rangle", "⟩"; + "\\rceil", "⌉"; + "\\registered", "®"; + "\\returnkey", "⏎"; + "\\revtabkey", "⇤"; + "\\rfloor", "⌋"; + "\\rhd", "⊳"; + "\\rho", "ρ"; + "\\rightarrow", "→"; + "\\rightarrowtail", "↣"; + "\\rightdelkey", "⌦"; + "\\rightharpoondown", "⇁"; + "\\rightharpoonup", "⇀"; + "\\rightleftarrows", "⇄"; + "\\rightleftharpoons", "⇌"; + "\\rightmoon", "☽"; + "\\rightrightarrows", "⇉"; + "\\rightsquigarrow", "⇝"; + "\\rightthreetimes", "⋌"; + "\\risingdotseq", "≓"; + "\\rtimes", "⋊"; + "\\sagittarius", "♐"; + "\\saturn", "♄"; + "\\scorpio", "♏"; + "\\searrow", "↘"; + "\\section", "§"; + "\\setminus", "∖"; + "\\sharp", "♯"; + "\\shiftkey", "⇧"; + "\\shortparallel", "∥"; + "\\sigma", "σ"; + "\\sim", "∼"; + "\\simeq", "≃"; + "\\smallfrown", "⌢"; + "\\smallsetminus", "∖"; + "\\smallsmile", "⌣"; + "\\smile", "⌣"; + "\\space", "␣"; + "\\spadesuit", "♠"; + "\\sphericalangle", "∢"; + "\\sqcap", "⊓"; + "\\sqcup", "⊔"; + "\\sqsubset", "⊏"; + "\\sqsubseteq", "⊑"; + "\\sqsupset", "⊐"; + "\\sqsupseteq", "⊒"; + "\\square", "□"; + "\\ss", "ß"; + "\\star", "⋆"; + "\\subset", "⊂"; + "\\subseteq", "⊆"; + "\\subsetneq", "⊊"; + "\\succ", "≻"; + "\\succcurlyeq", "≽"; + "\\succeq", "≽"; + "\\succsim", "≿"; + "\\sum", "∑"; + "\\supset", "⊃"; + "\\supseteq", "⊇"; + "\\supsetneq", "⊋"; + "\\surd", "√"; + "\\swarrow", "↙"; + "\\tabkey", "⇥"; + "\\tau", "τ"; + "\\taurus", "♉"; + "\\textbabygamma", "ɤ"; + "\\textbarglotstop", "ʡ"; + "\\textbari", "ɨ"; + "\\textbaro", "ɵ"; + "\\textbarrevglotstop", "ʢ"; + "\\textbaru", "ʉ"; + "\\textbeltl", "ɬ"; + "\\textbeta", "β"; + "\\textbullseye", "ʘ"; + "\\textchi", "χ"; + "\\textcloserevepsilon", "ɞ"; + "\\textcrh", "ħ"; + "\\textctc", "ɕ"; + "\\textctj", "ʝ"; + "\\textctz", "ʑ"; + "\\textdoublepipe", "ǁ"; + "\\textdyoghlig", "ʤ"; + "\\textepsilon", "ɛ"; + "\\textesh", "ʃ"; + "\\textfishhookr", "ɾ"; + "\\textgamma", "ɣ"; + "\\textglotstop", "ʔ"; + "\\textgrgamma", "γ"; + "\\texthtb", "ɓ"; + "\\texthtd", "ɗ"; + "\\texthtg", "ɠ"; + "\\texthth", "ɦ"; + "\\texththeng", "ɧ"; + "\\texthtscg", "ʛ"; + "\\textinvscr", "ʁ"; + "\\textiota", "ι"; + "\\textltailm", "ɱ"; + "\\textltailn", "ɲ"; + "\\textltilde", "ɫ"; + "\\textlyoghlig", "ɮ"; + "\\textopeno", "ɔ"; + "\\textphi", "ɸ"; + "\\textpipe", "ǀ"; + "\\textregistered", "®"; + "\\textreve", "ɘ"; + "\\textrevepsilon", "ɜ"; + "\\textrevglotstop", "ʕ"; + "\\textrhookrevepsilon", "ɝ"; + "\\textrighthookschwa", "ɚ"; + "\\textteshlig", "ʧ"; + "\\texttheta", "θ"; + "\\texttrademark", "™"; + "\\textturna", "ɐ"; + "\\textturnh", "ɥ"; + "\\textturnlonglegr", "ɺ"; + "\\textturnm", "ɯ"; + "\\textturnmrleg", "ɰ"; + "\\textturnr", "ɹ"; + "\\textturnrrtail", "ɻ"; + "\\textturnscripta", "ɒ"; + "\\textturnv", "ʌ"; + "\\textturnw", "ʍ"; + "\\textturny", "ʎ"; + "\\textupsilon", "ʊ"; + "\\textyogh", "ʒ"; + "\\th", "þ"; + "\\therefore", "∴"; + "\\theta", "θ"; + "\\h", "θ"; + "\\thickapprox", "≈"; + "\\thicksim", "∼"; + "\\times", "×"; + "\\top", "⊤"; + "\\trademark", "™"; + "\\triangle", "△"; + "\\triangledown", "▽"; + "\\triangleleft", "◁"; + "\\trianglelefteq", "⊴"; + "\\triangleq", "≜"; + "\\triangleright", "▷"; + "\\trianglerighteq", "⊵"; + "\\twoheadleftarrow", "↞"; + "\\twoheadrightarrow", "↠"; + "\\unlhd", "⊴"; + "\\unrhd", "⊵"; + "\\uparrow", "↑"; + "\\updownarrow", "↕"; + "\\upharpoonleft", "↿"; + "\\upharpoonright", "↾"; + "\\uplus", "⊎"; + "\\upsilon", "υ"; + "\\upuparrows", "⇈"; + "\\uranus", "⛢"; + "\\vDash", "⊨"; + "\\varepsilon", "ε"; + "\\varkappa", "ϰ"; + "\\varnothing", "∅"; + "\\varphi", "ϕ"; + "\\varpi", "ϖ"; + "\\varpropto", "∝"; + "\\varrho", "ϱ"; + "\\varsigma", "ς"; + "\\vartheta", "ϑ"; + "\\vartriangle", "△"; + "\\vartriangleleft", "⊲"; + "\\vartriangleright", "⊳"; + "\\vdash", "⊢"; + "\\vdots", "⋮"; + "\\vee", "∨"; + "\\veebar", "⊻"; + "\\venus", "♀"; + "\\virgo", "♍"; + "\\wedge", "∧"; + "\\whitebishop", "♗"; + "\\whiteking", "♔"; + "\\whiteknight", "♘"; + "\\whitepawn", "♙"; + "\\whitequeen", "♕"; + "\\whiterook", "♖"; + "\\wp", "℘"; + "\\wr", "≀"; + "\\xi", "ξ"; + "\\zeta", "ζ"; + + (** Double accent *) + "\\\"A", "Ä"; + "\\\"E", "Ë"; + "\\\"H", "Ḧ"; + "\\\"I", "Ï"; + "\\\"O", "Ö"; + "\\\"U", "Ü"; + "\\\"W", "Ẅ"; + "\\\"X", "Ẍ"; + "\\\"Y", "Ÿ"; + "\\\"a", "ä"; + "\\\"e", "ë"; + "\\\"h", "ḧ"; + "\\\"i", "ï"; + "\\\"o", "ö"; + "\\\"t", "ẗ"; + "\\\"u", "ü"; + "\\\"w", "ẅ"; + "\\\"x", "ẍ"; + "\\\"y", "ÿ"; + + (** Acute accent *) + "\\'A", "Á"; + "\\'C", "Ć"; + "\\'E", "É"; + "\\'G", "Ǵ"; + "\\'I", "Í"; + "\\'K", "Ḱ"; + "\\'L", "Ĺ"; + "\\'M", "Ḿ"; + "\\'N", "Ń"; + "\\'O", "Ó"; + "\\'P", "Ṕ"; + "\\'R", "Ŕ"; + "\\'S", "Ś"; + "\\'U", "Ú"; + "\\'W", "Ẃ"; + "\\'Y", "Ý"; + "\\'Z", "Ź"; + "\\'a", "á"; + "\\'c", "ć"; + "\\'e", "é"; + "\\'g", "ǵ"; + "\\'i", "í"; + "\\'k", "ḱ"; + "\\'l", "ĺ"; + "\\'m", "ḿ"; + "\\'n", "ń"; + "\\'o", "ó"; + "\\'p", "ṕ"; + "\\'r", "ŕ"; + "\\'s", "ś"; + "\\'u", "ú"; + "\\'w", "ẃ"; + "\\'y", "ý"; + "\\'z", "ź"; + + (** Doted accent *) + "\\.A", "Ȧ"; + "\\.B", "Ḃ"; + "\\.C", "Ċ"; + "\\.D", "Ḋ"; + "\\.E", "Ė"; + "\\.F", "Ḟ"; + "\\.G", "Ġ"; + "\\.H", "Ḣ"; + "\\.I", "İ"; + "\\.M", "Ṁ"; + "\\.N", "Ṅ"; + "\\.O", "Ȯ"; + "\\.P", "Ṗ"; + "\\.R", "Ṙ"; + "\\.S", "Ṡ"; + "\\.T", "Ṫ"; + "\\.W", "Ẇ"; + "\\.X", "Ẋ"; + "\\.Y", "Ẏ"; + "\\.Z", "Ż"; + "\\.a", "ȧ"; + "\\.b", "ḃ"; + "\\.c", "ċ"; + "\\.d", "ḋ"; + "\\.e", "ė"; + "\\.f", "ḟ"; + "\\.g", "ġ"; + "\\.h", "ḣ"; + "\\.m", "ṁ"; + "\\.n", "ṅ"; + "\\.o", "ȯ"; + "\\.p", "ṗ"; + "\\.r", "ṙ"; + "\\.s", "ṡ"; + "\\.t", "ṫ"; + "\\.w", "ẇ"; + "\\.x", "ẋ"; + "\\.y", "ẏ"; + "\\.z", "ż"; + "\\doteq", "≐"; + "\\doteqdot", "≑"; + "\\dotplus", "∔"; + "\\dotA", "Ȧ"; + "\\dotB", "Ḃ"; + "\\dotC", "Ċ"; + "\\dotD", "Ḋ"; + "\\dotE", "Ė"; + "\\dotF", "Ḟ"; + "\\dotG", "Ġ"; + "\\dotH", "Ḣ"; + "\\dotI", "İ"; + "\\dotM", "Ṁ"; + "\\dotN", "Ṅ"; + "\\dotO", "Ȯ"; + "\\dotP", "Ṗ"; + "\\dotR", "Ṙ"; + "\\dotS", "Ṡ"; + "\\dotT", "Ṫ"; + "\\dotW", "Ẇ"; + "\\dotX", "Ẋ"; + "\\dotY", "Ẏ"; + "\\dotZ", "Ż"; + "\\dota", "ȧ"; + "\\dotb", "ḃ"; + "\\dotc", "ċ"; + "\\dotd", "ḋ"; + "\\dote", "ė"; + "\\dotf", "ḟ"; + "\\dotg", "ġ"; + "\\doth", "ḣ"; + "\\dotm", "ṁ"; + "\\dotn", "ṅ"; + "\\doto", "ȯ"; + "\\dotp", "ṗ"; + "\\dotr", "ṙ"; + "\\dots", "ṡ"; + "\\dott", "ṫ"; + "\\dotw", "ẇ"; + "\\dotx", "ẋ"; + "\\doty", "ẏ"; + "\\dotz", "ż"; + "\\dA", "Ạ"; + "\\dB", "Ḅ"; + "\\dD", "Ḍ"; + "\\dE", "Ẹ"; + "\\dH", "Ḥ"; + "\\dI", "Ị"; + "\\dK", "Ḳ"; + "\\dL", "Ḷ"; + "\\dM", "Ṃ"; + "\\dN", "Ṇ"; + "\\dO", "Ọ"; + "\\dR", "Ṛ"; + "\\dS", "Ṣ"; + "\\dT", "Ṭ"; + "\\dU", "Ụ"; + "\\dV", "Ṿ"; + "\\dW", "Ẉ"; + "\\dY", "Ỵ"; + "\\dZ", "Ẓ"; + "\\da", "ạ"; + "\\db", "ḅ"; + "\\dd", "ḍ"; + "\\de", "ẹ"; + "\\dh", "ḥ"; + "\\di", "ị"; + "\\dk", "ḳ"; + "\\dl", "ḷ"; + "\\dm", "ṃ"; + "\\dn", "ṇ"; + "\\do", "ọ"; + "\\dr", "ṛ"; + "\\ds", "ṣ"; + "\\dt", "ṭ"; + "\\du", "ụ"; + "\\dv", "ṿ"; + "\\dw", "ẉ"; + "\\dy", "ỵ"; + "\\dz", "ẓ"; + + (** Double dot accent *) + "\\ddots", "⋱"; + "\\ddotA", "Ä"; + "\\ddotE", "Ë"; + "\\ddotH", "Ḧ"; + "\\ddotI", "Ï"; + "\\ddotO", "Ö"; + "\\ddotU", "Ü"; + "\\ddotW", "Ẅ"; + "\\ddotX", "Ẍ"; + "\\ddotY", "Ÿ"; + "\\ddota", "ä"; + "\\ddote", "ë"; + "\\ddoth", "ḧ"; + "\\ddoti", "ï"; + "\\ddoto", "ö"; + "\\ddott", "ẗ"; + "\\ddotu", "ü"; + "\\ddotw", "ẅ"; + "\\ddotx", "ẍ"; + "\\ddoty", "ÿ"; + + (** Breve accent *) + "\\breveA", "Ă"; + "\\breveE", "Ĕ"; + "\\breveG", "Ğ"; + "\\breveI", "Ĭ"; + "\\breveO", "Ŏ"; + "\\breveU", "Ŭ"; + "\\brevea", "ă"; + "\\brevee", "ĕ"; + "\\breveg", "ğ"; + "\\brevei", "ĭ"; + "\\breveo", "ŏ"; + "\\breveu", "ŭ"; + "\\uA", "Ă"; + "\\uE", "Ĕ"; + "\\uG", "Ğ"; + "\\uI", "Ĭ"; + "\\uO", "Ŏ"; + "\\uU", "Ŭ"; + "\\ua", "ă"; + "\\ue", "ĕ"; + "\\ug", "ğ"; + "\\ui", "ĭ"; + "\\uo", "ŏ"; + "\\uu", "ŭ"; + + (** Check accent *) + "\\checkA", "Ǎ"; + "\\checkC", "Č"; + "\\checkD", "Ď"; + "\\checkE", "Ě"; + "\\checkN", "Ň"; + "\\checkR", "Ř"; + "\\checkS", "Š"; + "\\checkT", "Ť"; + "\\checkZ", "Ž"; + "\\checka", "ǎ"; + "\\checkc", "č"; + "\\checkd", "ď"; + "\\checke", "ě"; + "\\checkn", "ň"; + "\\checkr", "ř"; + "\\checks", "š"; + "\\checkt", "ť"; + "\\checkz", "ž"; + "\\vA", "Ǎ"; + "\\vC", "Č"; + "\\vD", "Ď"; + "\\vE", "Ě"; + "\\vN", "Ň"; + "\\vR", "Ř"; + "\\vS", "Š"; + "\\vT", "Ť"; + "\\vZ", "Ž"; + "\\va", "ǎ"; + "\\vc", "č"; + "\\vd", "ď"; + "\\ve", "ě"; + "\\vn", "ň"; + "\\vr", "ř"; + "\\vs", "š"; + "\\vt", "ť"; + "\\vz", "ž"; + + (** Bar accent *) + "\\=A", "Ā"; + "\\=E", "Ē"; + "\\=G", "Ḡ"; + "\\=I", "Ī"; + "\\=O", "Ō"; + "\\=U", "Ū"; + "\\=Y", "Ȳ"; + "\\=a", "ā"; + "\\=e", "ē"; + "\\=g", "ḡ"; + "\\=i", "ī"; + "\\=o", "ō"; + "\\=u", "ū"; + "\\=y", "ȳ"; + "\\AA", "Å"; + "\\AE", "Æ"; + "\\barA", "Ā"; + "\\barE", "Ē"; + "\\barG", "Ḡ"; + "\\barI", "Ī"; + "\\barO", "Ō"; + "\\barU", "Ū"; + "\\barY", "Ȳ"; + "\\bara", "ā"; + "\\bare", "ē"; + "\\barg", "ḡ"; + "\\bari", "ī"; + "\\baro", "ō"; + "\\baru", "ū"; + "\\bary", "ȳ"; + + (** Hat acccent *) + "\\^A", "Â"; + "\\^C", "Ĉ"; + "\\^E", "Ê"; + "\\^G", "Ĝ"; + "\\^H", "Ĥ"; + "\\^I", "Î"; + "\\^J", "Ĵ"; + "\\^O", "Ô"; + "\\^S", "Ŝ"; + "\\^U", "Û"; + "\\^W", "Ŵ"; + "\\^Y", "Ŷ"; + "\\^Z", "Ẑ"; + "\\^a", "â"; + "\\^c", "ĉ"; + "\\^e", "ê"; + "\\^g", "ĝ"; + "\\^h", "ĥ"; + "\\^i", "î"; + "\\^j", "ĵ"; + "\\^o", "ô"; + "\\^s", "ŝ"; + "\\^u", "û"; + "\\^w", "ŵ"; + "\\^y", "ŷ"; + "\\^z", "ẑ"; + + (** Backquote acccent *) + "\\`A", "À"; + "\\`E", "È"; + "\\`I", "Ì"; + "\\`N", "Ǹ"; + "\\`O", "Ò"; + "\\`U", "Ù"; + "\\`W", "Ẁ"; + "\\`Y", "Ỳ"; + "\\`a", "à"; + "\\`e", "è"; + "\\`i", "ì"; + "\\`n", "ǹ"; + "\\`o", "ò"; + "\\`u", "ù"; + "\\`w", "ẁ"; + "\\`y", "ỳ"; + + (** Tiled acccent *) + "\\~A", "Ā"; + "\\~E", "Ẽ"; + "\\~I", "Ĩ"; + "\\~N", "Ñ"; + "\\~O", "Õ"; + "\\~U", "Ũ"; + "\\~Y", "Ỹ"; + "\\~a", "ã"; + "\\~e", "ẽ"; + "\\~i", "ĩ"; + "\\~n", "ñ"; + "\\~o", "õ"; + "\\~u", "ũ"; + "\\~y", "ỹ"; + + (** textrt font *) + "\\textrtaild", "ɖ"; + "\\textrtaill", "ɭ"; + "\\textrtailn", "ɳ"; + "\\textrtailr", "ɽ"; + "\\textrtails", "ʂ"; + "\\textrtailt", "ʈ"; + "\\textrtailz", "ʐ"; + + (** textsc font *) + "\\textscb", "ʙ"; + "\\textscg", "ɢ"; + "\\textsch", "ʜ"; + "\\textschwa", "ə"; + "\\textsci", "ɪ"; + "\\textscl", "ʟ"; + "\\textscn", "ɴ"; + "\\textscoelig", "ɶ"; + "\\textscr", "ʀ"; + "\\textscripta", "ɑ"; + "\\textscriptv", "ʋ"; + "\\textscy", "ʏ"; + + (** bb font *) + "\\bb0", "𝟘"; + "\\bb1", "𝟙"; + "\\bb2", "𝟚"; + "\\bb3", "𝟛"; + "\\bb4", "𝟜"; + "\\bb5", "𝟝"; + "\\bb6", "𝟞"; + "\\bb7", "𝟟"; + "\\bb8", "𝟠"; + "\\bb9", "𝟡"; + "\\bbA", "𝔸"; + "\\bbB", "𝔹"; + "\\bbC", "ℂ"; + "\\bbD", "𝔻"; + "\\bbE", "𝔼"; + "\\bbF", "𝔽"; + "\\bbG", "𝔾"; + "\\bbH", "ℍ"; + "\\bbI", "𝕀"; + "\\bbJ", "𝕁"; + "\\bbK", "𝕂"; + "\\bbL", "𝕃"; + "\\bbM", "𝕄"; + "\\bbN", "ℕ"; + "\\bbO", "𝕆"; + "\\bbP", "ℙ"; + "\\bbQ", "ℚ"; + "\\bbR", "ℝ"; + "\\bbS", "𝕊"; + "\\bbT", "𝕋"; + "\\bbU", "𝕌"; + "\\bbV", "𝕍"; + "\\bbW", "𝕎"; + "\\bbX", "𝕏"; + "\\bbY", "𝕐"; + "\\bbZ", "ℤ"; + "\\bba", "𝕒"; + "\\bbb", "𝕓"; + "\\bbc", "𝕔"; + "\\bbd", "𝕕"; + "\\bbe", "𝕖"; + "\\bbf", "𝕗"; + "\\bbg", "𝕘"; + "\\bbh", "𝕙"; + "\\bbi", "𝕚"; + "\\bbj", "𝕛"; + "\\bbk", "𝕜"; + "\\bbl", "𝕝"; + "\\bbm", "𝕞"; + "\\bbn", "𝕟"; + "\\bbo", "𝕠"; + "\\bbp", "𝕡"; + "\\bbq", "𝕢"; + "\\bbr", "𝕣"; + "\\bbs", "𝕤"; + "\\bbt", "𝕥"; + "\\bbu", "𝕦"; + "\\bbv", "𝕧"; + "\\bbw", "𝕨"; + "\\bbx", "𝕩"; + "\\bby", "𝕪"; + "\\bbz", "𝕫"; + + (** cal font *) + "\\calA", "𝒜"; + "\\calB", "ℬ"; + "\\calC", "𝒞"; + "\\calD", "𝒟"; + "\\calE", "ℰ"; + "\\calF", "ℱ"; + "\\calG", "𝒢"; + "\\calH", "ℋ"; + "\\calI", "ℐ"; + "\\calJ", "𝒥"; + "\\calK", "𝒦"; + "\\calL", "ℒ"; + "\\calM", "ℳ"; + "\\calN", "𝒩"; + "\\calO", "𝒪"; + "\\calP", "𝒫"; + "\\calQ", "𝒬"; + "\\calR", "ℛ"; + "\\calS", "𝒮"; + "\\calT", "𝒯"; + "\\calU", "𝒰"; + "\\calV", "𝒱"; + "\\calW", "𝒲"; + "\\calX", "𝒳"; + "\\calY", "𝒴"; + "\\calZ", "𝒵"; + "\\cala", "𝒶"; + "\\calb", "𝒷"; + "\\calc", "𝒸"; + "\\cald", "𝒹"; + "\\cale", "ℯ"; + "\\calf", "𝒻"; + "\\calg", "ℊ"; + "\\calh", "𝒽"; + "\\cali", "𝒾"; + "\\calj", "𝒿"; + "\\calk", "𝓀"; + "\\call", "𝓁"; + "\\calm", "𝓂"; + "\\caln", "𝓃"; + "\\calo", "ℴ"; + "\\calp", "𝓅"; + "\\calq", "𝓆"; + "\\calr", "𝓇"; + "\\cals", "𝓈"; + "\\calt", "𝓉"; + "\\calu", "𝓊"; + "\\calv", "𝓋"; + "\\calw", "𝓌"; + "\\calx", "𝓍"; + "\\caly", "𝓎"; + "\\calz", "𝓏"; + + (** frak font *) + "\\frakA", "𝔄"; + "\\frakB", "𝔅"; + "\\frakC", "ℭ"; + "\\frakD", "𝔇"; + "\\frakE", "𝔈"; + "\\frakF", "𝔉"; + "\\frakG", "𝔊"; + "\\frakH", "ℌ"; + "\\frakI", "ℑ"; + "\\frakJ", "𝔍"; + "\\frakK", "𝔎"; + "\\frakL", "𝔏"; + "\\frakM", "𝔐"; + "\\frakN", "𝔑"; + "\\frakO", "𝔒"; + "\\frakP", "𝔓"; + "\\frakQ", "𝔔"; + "\\frakR", "ℜ"; + "\\frakS", "𝔖"; + "\\frakT", "𝔗"; + "\\frakU", "𝔘"; + "\\frakV", "𝔙"; + "\\frakW", "𝔚"; + "\\frakX", "𝔛"; + "\\frakY", "𝔜"; + "\\frakZ", "ℨ"; + "\\fraka", "𝔞"; + "\\frakb", "𝔟"; + "\\frakc", "𝔠"; + "\\frakd", "𝔡"; + "\\frake", "𝔢"; + "\\frakf", "𝔣"; + "\\frakg", "𝔤"; + "\\frakh", "𝔥"; + "\\fraki", "𝔦"; + "\\frakj", "𝔧"; + "\\frakk", "𝔨"; + "\\frakl", "𝔩"; + "\\frakm", "𝔪"; + "\\frakn", "𝔫"; + "\\frako", "𝔬"; + "\\frakp", "𝔭"; + "\\frakq", "𝔮"; + "\\frakr", "𝔯"; + "\\fraks", "𝔰"; + "\\frakt", "𝔱"; + "\\fraku", "𝔲"; + "\\frakv", "𝔳"; + "\\frakw", "𝔴"; + "\\frakx", "𝔵"; + "\\fraky", "𝔶"; + "\\frakz", "𝔷"; + + (** Exponent *) + "\\^(", "⁽"; + "\\^)", "⁾"; + "\\^+", "⁺"; + "\\^-", "⁻"; + "\\^0", "⁰"; + "\\^1", "¹"; + "\\^2", "²"; + "\\^3", "³"; + "\\^4", "⁴"; + "\\^5", "⁵"; + "\\^6", "⁶"; + "\\^7", "⁷"; + "\\^8", "⁸"; + "\\^9", "⁹"; + "\\^=", "⁼"; + "\\^A", "ᴬ"; + "\\^B", "ᴮ"; + "\\^D", "ᴰ"; + "\\^E", "ᴱ"; + "\\^G", "ᴳ"; + "\\^H", "ᴴ"; + "\\^I", "ᴵ"; + "\\^J", "ᴶ"; + "\\^K", "ᴷ"; + "\\^L", "ᴸ"; + "\\^M", "ᴹ"; + "\\^N", "ᴺ"; + "\\^O", "ᴼ"; + "\\^P", "ᴾ"; + "\\^R", "ᴿ"; + "\\^T", "ᵀ"; + "\\^U", "ᵁ"; + "\\^V", "ⱽ"; + "\\^W", "ᵂ"; + "\\^alpha", "ᵅ"; + "\\^beta", "ᵝ"; + "\\^chi", "ᵡ"; + "\\^delta", "ᵟ"; + "\\^epsilon", "ᵋ"; + "\\^gamma", "ᵞ"; + "\\^iota", "ᶥ"; + "\\^phi", "ᶲ"; + "\\^theta", "ᶿ"; + "\\^varphi", "ᵠ"; + "\\^a", "ᵃ"; + "\\^b", "ᵇ"; + "\\^c", "ᶜ"; + "\\^d", "ᵈ"; + "\\^e", "ᵉ"; + "\\^f", "ᶠ"; + "\\^g", "ᵍ"; + "\\^h", "ʰ"; + "\\^i", "ⁱ"; + "\\^j", "ʲ"; + "\\^k", "ᵏ"; + "\\^l", "ˡ"; + "\\^m", "ᵐ"; + "\\^n", "ⁿ"; + "\\^o", "ᵒ"; + "\\^p", "ᵖ"; + "\\^r", "ʳ"; + "\\^s", "ˢ"; + "\\^t", "ᵗ"; + "\\^u", "ᵘ"; + "\\^v", "ᵛ"; + "\\^w", "ʷ"; + "\\^x", "ˣ"; + "\\^y", "ʸ"; + "\\^z", "ᶻ"; + + (** Subscript *) + "\\_(", "₍"; + "\\_)", "₎"; + "\\_+", "₊"; + "\\_-", "₋"; + "\\_0", "₀"; + "\\_1", "₁"; + "\\_2", "₂"; + "\\_3", "₃"; + "\\_4", "₄"; + "\\_5", "₅"; + "\\_6", "₆"; + "\\_7", "₇"; + "\\_8", "₈"; + "\\_9", "₉"; + "\\_=", "₌"; + "\\_beta", "ᵦ"; + "\\_chi", "ᵪ"; + "\\_gamma", "ᵧ"; + "\\_rho", "ᵨ"; + "\\_varphi", "ᵩ"; + "\\_a", "ₐ"; + "\\_e", "ₑ"; + "\\_h", "ₕ"; + "\\_i", "ᵢ"; + "\\_j", "ⱼ"; + "\\_k", "ₖ"; + "\\_l", "ₗ"; + "\\_m", "ₘ"; + "\\_n", "ₙ"; + "\\_o", "ₒ"; + "\\_p", "ₚ"; + "\\_r", "ᵣ"; + "\\_s", "ₛ"; + "\\_t", "ₜ"; + "\\_u", "ᵤ"; + "\\_v", "ᵥ"; + "\\_x", "ₓ"; + +] + + +(** **************************************************************************) +(** * Priorities *) + +(** Set priorities, at the moment only for greek letters *) + +let priorities = [ +(* {{{ greek letters *) + "\\alpha", 1; + "\\beta", 1; + "\\gamma", 1; + "\\delta", 1; + "\\epsilon", 1; + "\\zeta", 1; + "\\eta", 2; + "\\theta", 2; + "\\iota", 1; + "\\kappa", 1; + "\\lambda", 1; + "\\mu", 1; + "\\nu", 1; + "\\xi", 1; + "\\o", 1; + "\\pi", 1; + "\\rho", 1; + "\\sigma", 1; + "\\tau", 1; + "\\upsilon", 1; + "\\phi", 2; + "\\chi", 1; + "\\psi", 2; + "\\omega", 2; + "\\Gamma", 1; + "\\Delta", 1; + "\\Theta", 2; + "\\Lambda", 1; + "\\Xi", 1; + "\\Pi", 1; + "\\Sigma", 1; + "\\Upsilon", 1; + "\\Phi", 2; + "\\Psi", 2; + "\\Omega", 1; +(* }}} *) +] + + +(** **************************************************************************) +(** * Binding generator *) + +let filename = + let args = Sys.argv in + if Array.length args < 2 + then failwith "please provide output filename as argument"; + Sys.argv.(1) + +let _ = (* generate output file *) + let bindings = ref [] in + let add (key,value) = + bindings := (key,value)::!bindings in + (* add bindings from set 1 *) + List.iter (fun (keys,value,_group) -> + List.iter (fun key -> add (key,value)) keys) bindings_set_1; + (* add bindings from set 2 *) + List.iter add bindings_set_2; + (* create table for priorities lookup *) + let priotable = Hashtbl.create 20 in + List.iter (fun (key,prio) -> Hashtbl.add priotable key prio) priorities; + (* remove duplicates and sort *) + let outbindings = List.sort_uniq (fun (key1,_) (key2,_) -> String.compare key1 key2) !bindings in + (* print bindings into file, including optional priorities *) + let file = open_out filename in + let print_binding (key,value) = + Printf.fprintf file "%s %s" key value; + begin match Hashtbl.find_opt priotable key with + | Some prio -> Printf.fprintf file " %d" prio + | None -> () + end; + Printf.fprintf file "\n" + in + List.iter print_binding outbindings; + close_out file + + +(** **************************************************************************) +(** * Groups of similar shapes *) + +(* For future use. + +let predefined_classes = [ + ["&"; "⅋"; ]; + ["|"; "∥"; ]; + ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ]; + ["?"; "¿"; "⸮"; ]; + [":"; "⁝"; ]; + ["."; "•"; "◦"; ]; + ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; + ["+"; "⊞"; ]; + ["-"; "÷"; "⊢"; "⊩"; "⊟"; ]; + ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; + ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; + ["^"; "↑"; ] ; + ["⇑"; "⇧"; "⬆"; ] ; + ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; + ["⇕"; "⇳"; "⬍"; ]; + ["↔"; "⇔"; "⬄"; "⬌"; ] ; + ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; + ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; + ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; + ["("; "❨"; "❪"; "❲"; "（"; ]; + [")"; "❩"; "❫"; "❳"; "）"; ]; + ["["; "⦋"; "〚"; ] ; + ["]"; "⦌"; "〛"; ] ; + ["{"; "❴"; "⦃" ] ; + ["}"; "❵"; "⦄" ] ; + ["□"; "◽"; "▪"; "◾"; ]; + ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; + [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; + ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; + ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; + ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; + ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; + ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; + ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ; + ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ; + ["C"; "ℭ"; "∁"; "𝐂"; "Ⓒ"; ] ; + ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ; + ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ; + ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ; + ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ; + ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ; + ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; ] ; + ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ; + ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ; + ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡"; "ⓗ"; ] ; + ["H"; "ℋ"; "ℍ"; "𝐇"; "Ⓗ"; ] ; + ["i"; "ι"; "ℐ"; "𝕚"; "ⅈ"; "𝐢"; "𝛊"; "ⓘ"; ] ; + ["I"; "𝕀"; "𝐈"; "Ⓘ"; ] ; + ["j"; "𝕛"; "𝐣"; "ⓙ"; ] ; + ["J"; "Ј"; "𝕁"; "𝐉"; "Ⓙ"; ] ; + ["k"; "κ"; "𝕜"; "𝐤"; "𝛋"; "ⓚ"; ] ; + ["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ; + ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ; + ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; ] ; + ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ; + ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ; + ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ; + ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; + ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; + ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; + ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ; + ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ; + ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ; + ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ; + ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ; + ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ; + ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ; + ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ; + ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ; + ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ; + ["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ; + ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ; + ["V"; "𝕍"; "𝐕"; "Ⓥ"; ] ; + ["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; "ⓦ"; ] ; + ["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; "Ⓦ"; ] ; + ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱"; "𝛏"; "𝛘"; "𝛞"; "ⓧ"; ] ; + ["X"; "Ξ"; "𝕏";"𝐗"; "𝚵"; "Ⓧ"; "⦻"; ] ; + ["y"; "υ"; "𝕪"; "𝐲"; "ⓨ"; ] ; + ["Y"; "ϒ"; "𝕐"; "𝐘"; "𝚼"; "Ⓨ"; ] ; + ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; "ⓩ"; ] ; + ["Z"; "ℨ"; "ℤ"; "𝐙"; "Ⓩ"; ] ; + ["0"; "𝟘"; "⓪"; ] ; + ["1"; "𝟙"; "①"; "⓵"; ] ; + ["2"; "𝟚"; "②"; "⓶"; ] ; + ["3"; "𝟛"; "③"; "⓷"; ] ; + ["4"; "𝟜"; "④"; "⓸"; ] ; + ["5"; "𝟝"; "⑤"; "⓹"; ] ; + ["6"; "𝟞"; "⑥"; "⓺"; ] ; + ["7"; "𝟟"; "⑦"; "⓻"; ] ; + ["8"; "𝟠"; "⑧"; "⓼"; "∞"; ] ; + ["9"; "𝟡"; "⑨"; "⓽"; ] ; + ] + +*) -- cgit v1.2.3 From 4625a6dc8a949a5fb7a9fdecd5e657ad638fefb1 Mon Sep 17 00:00:00 2001 From: charguer Date: Mon, 12 Nov 2018 17:10:11 +0100 Subject: bindings files storage --- ide/coqide.ml | 1 - ide/preferences.ml | 68 +++++++++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 60 insertions(+), 9 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index bc3f5212f6..e79e11540e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1386,7 +1386,6 @@ let read_coqide_args argv = |[] -> (coqtop,project_files,bindings_files,List.rev out) in let coqtop,project_files,bindings_files,argv = filter_coqtop None None [] [] argv in - let bindings_files = if bindings_files = [] then ["default"] else bindings_files in Ideutils.custom_coqtop := coqtop; custom_project_file := project_files; Preferences.load_unicode_bindings_files bindings_files; diff --git a/ide/preferences.ml b/ide/preferences.ml index 57589b4363..7cca715dc3 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -249,9 +249,15 @@ let loaded_accel_file = try get_config_file "coqide.keys" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" -let loaded_default_unicode_bindings_file = - try get_config_file "coqide.bindings" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings" +let get_bindings_local_file () = + try Some (get_config_file "coqide.bindings") + with Not_found -> None + +let get_bindings_default_file () = + let ( / ) = Filename.concat in + let path = Envars.coqlib () / "ide/default.bindings" in + Printf.eprintf "==> %s\n" path; + if Sys.file_exists path then Some path else None (** Hooks *) @@ -1030,7 +1036,7 @@ let configure ?(apply=(fun () -> ())) parent = \lambda λ 3 \lambdas λs 4 \lake Ο 2 - \lemma "Lemma foo : x. Proof. Qed." 1 ---currently not supported by parser + \lemma "Lemma foo : x. Proof. Qed." 1 ---currently not supported by the parser - In case of equality between two candidates (same ascii word, or same priorities for two words with similar prefix), the first binding is considered. @@ -1074,15 +1080,61 @@ let process_unicode_bindings_file filename = close_in ch let load_unicode_bindings_files filenames = - let filenames = List.map (fun f -> - if f = "default" then loaded_default_unicode_bindings_file else f) filenames in - List.iter process_unicode_bindings_file filenames; + let selected_filenames = ref [] in + let add f = + selected_filenames := f::!selected_filenames in + if filenames = [] then begin + (* If no argument is provided using [-unicode-bindings], + then use the default file and the local file, if it exists *) + begin match get_bindings_default_file() with + | Some f -> add f + | None -> output_string stderr (Printf.sprintf "Warning: the file ide/default.bindings was not found in %s.\n" (Envars.coqlib())) + (* TODO: flush stderr does not seem to eagerly display the output message *) + end; + begin match get_bindings_local_file() with + | Some f -> add f + | None -> () + end; + end else begin + (* If [-unicode-bindings] is used with a list of file, consider + these files in order, with a special treatment for the tokens + "default" and "local", which are replaced by the appropriate path. *) + let add_arg f = + match f with + | "default" -> + begin match get_bindings_default_file() with + | Some f -> add f + | None -> output_string stderr (Printf.sprintf "Error:the file ide/default.bindings was not found in %s.\n" (Envars.coqlib())); exit 1 + end + | "local" -> + begin match get_bindings_local_file() with + | Some f -> add f + | None -> output_string stderr (Printf.sprintf "Error: the local configuration file coqide.bindings was not found.\n"); exit 1 + end + | _ -> add f + in + List.iter add_arg filenames + end; + (* Files must be processed in order, to build the list of bindings + by iteratively consing entry to its head, the list being reversed + at the very end *) + let real_filenames = List.rev !selected_filenames in + List.iter process_unicode_bindings_file real_filenames; unicode_bindings := List.rev !unicode_bindings - (* For debugging unicode bindings: + (* For debugging the list of unicode files loaded: + List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames; + *) + (* For debugging the list of unicode bindings loaded: let print_unicode_bindings () = List.iter (fun (x,y,p) -> Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) !unicode_bindings; prerr_newline() *) + + (* TODO: known issue: the "~" in path of several arguments does + not seem to be correctly interpreted, e.g. + bin/coqide -unicode-bindings local,~/.config/coq/my.bindings & + Possible fix is to expand first to absolute paths. + *) -- cgit v1.2.3 From 3149d03bd4e8879045819d6cfc67ae4e0ccaf1fc Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 13 Nov 2018 10:32:02 +0100 Subject: implementation installation of default unicode bindings --- Makefile.ide | 4 ++-- ide/preferences.ml | 10 ++++++---- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/Makefile.ide b/Makefile.ide index f26c9bd282..efbc9ef389 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -218,7 +218,7 @@ endif install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi @@ -246,7 +246,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(MKDIR) $@/coq/ - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $@/coq/ $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ diff --git a/ide/preferences.ml b/ide/preferences.ml index 7cca715dc3..205961261a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -254,10 +254,12 @@ let get_bindings_local_file () = with Not_found -> None let get_bindings_default_file () = - let ( / ) = Filename.concat in - let path = Envars.coqlib () / "ide/default.bindings" in - Printf.eprintf "==> %s\n" path; - if Sys.file_exists path then Some path else None + let name = "default.bindings" in + let chk d = Sys.file_exists (Filename.concat d name) in + try + let dir = List.find chk (Minilib.coqide_data_dirs ()) in + Some (Filename.concat dir name) + with Not_found -> None (** Hooks *) -- cgit v1.2.3 From ea789fb00cecbb720702940d4752e991bbcc2054 Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 13 Nov 2018 11:04:00 +0100 Subject: documentation for unicode bindings --- doc/sphinx/practical-tools/coqide.rst | 76 +++++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 25 deletions(-) diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 8b7fe20191..ab7fe2ac08 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -218,7 +218,8 @@ Using Unicode symbols |CoqIDE| is based on GTK+ and inherits from it support for Unicode in its text windows. Consequently a large set of symbols is available for -notations. +notations. Furthermore, |CoqIDE| conveniently provides a simple way to +input Unicode characters. Displaying Unicode symbols @@ -254,37 +255,62 @@ use antialiased fonts or not, by setting the environment variable Defining an input method for non-ASCII symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To input a Unicode symbol, a general method provided by GTK+ is to -simultaneously press the Control, Shift and “u” keys, release, then -type the hexadecimal code of the symbol required, for example `2200` -for the ∀ symbol. A list of symbol codes is available at -`http://www.unicode.org`. +CoqIDE supports a builtin mechanism to input non-ASCII symbols. +For example, to input ``π``, it suffices to type ``\pi`` then press the +combination of key ``Shift+Space`` (default key binding). Often, it +suffices to type a prefix of the latex token, e.g. typing ``\p`` +then ``Shift+Space`` suffices to insert a ``π``. -An alternative method which does not require to know the hexadecimal -code of the character is to use an Input Method Editor. On POSIX -systems (Linux distributions, BSD variants and MacOS X), you can -use `uim` version 1.6 or later which provides a LaTeX-style input -method. +For several symbols, ASCII art is also recognized, e.g. ``\->`` for a +right arrow, or ``\>=`` for a greater than or equal sign. -To configure uim, execute uim-pref-gtk as your regular user. In the -"Global Settings" group set the default Input Method to "ELatin" -(don’t forget to tick the checkbox "Specify default IM"). In the -"ELatin" group set the layout to "TeX", and remember the content of -the "[ELatin] on" field (by default Control-\\). You can now execute -|CoqIDE| with the following commands (assuming you use a Bourne-style -shell): +A larger number of latex tokens are supported by default. The full list +is available here: +https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml -:: +Custom bindings may be added, as explained further on. - $ export GTK_IM_MODULE=uim - $ coqide +Remark: it remains possible to input non-ASCII symbols using system-wide +approaches independent of |CoqIDE|. -Activate the ELatin Input Method with Control-\\, then type the -sequence `\\Gamma`. You will see the sequence being replaced by Γ as -soon as you type the second "a". +Adding custom bindings +~~~~~~~~~~~~~~~~~~~~~~ + +To extend the default set of bindings, create a file named `coqide.bindings` +and place it in the same folder as `coqide.keys`. On Linux, this would be +the folder ``~/.config/coq``. The file `coqide.bindings` should contain one +binding per line, in the form ``\key value``, followed by an optional priority +integer. (The key and value should not contain any space character.) +Here is an example configuration file: + +``` +\par || +\pi π 1 +\le ≤ 1 +\lambda λ 2 +\lambdas λs +``` + +Above, the priority number 1 on ``\pi`` indicates that the prefix ``\p`` +should resolve to ``\pi``, and not to something else (e.g. ``\par``). +Similarly, the above settings ensure than ``\l`` resolves to ``\le``, +and that ``\la`` resolves to ``\lambda``. + +It can be useful to work with per-project binding files. For this purpose +|CoqIDE| accepts a command line argument of the form +``-unicode-bindings file1,file2,...,fileN``. +Each of the file tokens provided may consists of one of: + + - a path to a custom bindings file, + - the token ``default``, which resolves to the default bindings file, + - the token ``local``, which resolves to the `coqide.bindings` file + stored in the user configuration directory. + +Remark: if two bindings for a same token both have the same priority value +(or both have no priority value set), then the binding considered is the +one from the file that comes first on the command line. -.. _character-encoding-saved-files: Character encoding for saved files ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 5ad4ed36e09416e8e4aa16f67b517eec78591532 Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 13 Nov 2018 11:12:51 +0100 Subject: Latex to LaTex --- ide/coqide.ml | 2 +- ide/coqide_ui.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index e79e11540e..8e62ac9193 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1165,7 +1165,7 @@ let build_ui () = ~callback:MiscMenu.uncomment; item "Coqtop arguments" ~label:"Coqtop _arguments" ~callback:MiscMenu.coqtop_arguments; - item "Latex-to-unicode" ~label:"_Latex-to-unicode" ~accel:"space" + item "LaTeX-to-unicode" ~label:"_LaTeX-to-unicode" ~accel:"space" ~callback:MiscMenu.apply_unicode_binding; ]; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index c30d6604d2..d4a339f4f5 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -141,7 +141,7 @@ let init () = \n \ \n \ \n \ -\n \ +\n \ \n \ \n \ \n \ -- cgit v1.2.3 From 8d93141a931a4007feb8f28df2cd61c7b1c1b61e Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 14 Nov 2018 12:53:38 +0100 Subject: final polishing for coqide bindings --- doc/sphinx/practical-tools/coqide.rst | 5 ++ ide/coqide.ml | 2 +- ide/ide.mllib | 1 + ide/preferences.ml | 125 +------------------------------- ide/preferences.mli | 7 +- ide/unicode_bindings.ml | 131 ++++++++++++++++++++++++++++++++++ ide/unicode_bindings.mli | 48 +++++++++++++ ide/wg_ScriptView.ml | 35 ++------- 8 files changed, 198 insertions(+), 156 deletions(-) create mode 100644 ide/unicode_bindings.ml create mode 100644 ide/unicode_bindings.mli diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index ab7fe2ac08..44955412ce 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -307,6 +307,11 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. +Remark: if a filename other than the first one includes a "~" to refer +to the home directory, it won't be expanded properly. To work around that +issue, one should not use comas but instead repeat the flag, in the form: +``-unicode-bindings file1 .. -unicode-bindings fileN``. + Remark: if two bindings for a same token both have the same priority value (or both have no priority value set), then the binding considered is the one from the file that comes first on the command line. diff --git a/ide/coqide.ml b/ide/coqide.ml index 8e62ac9193..e16c7db3b4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1388,7 +1388,7 @@ let read_coqide_args argv = let coqtop,project_files,bindings_files,argv = filter_coqtop None None [] [] argv in Ideutils.custom_coqtop := coqtop; custom_project_file := project_files; - Preferences.load_unicode_bindings_files bindings_files; + Unicode_bindings.load_files bindings_files; argv diff --git a/ide/ide.mllib b/ide/ide.mllib index a7ade71307..f8a2d77be8 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -11,6 +11,7 @@ Preferences Project_file Topfmt Ideutils +Unicode_bindings Coq Coq_lex Sentence diff --git a/ide/preferences.ml b/ide/preferences.ml index 205961261a..27f240a993 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -249,11 +249,11 @@ let loaded_accel_file = try get_config_file "coqide.keys" with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" -let get_bindings_local_file () = +let get_unicode_bindings_local_file () = try Some (get_config_file "coqide.bindings") with Not_found -> None -let get_bindings_default_file () = +let get_unicode_bindings_default_file () = let name = "default.bindings" in let chk d = Sys.file_exists (Filename.concat d name) in try @@ -1019,124 +1019,3 @@ let configure ?(apply=(fun () -> ())) parent = match x with | Return_apply | Return_ok -> save_pref () | Return_cancel -> () - -(********************************************************************) - -(** Latex to unicode bindings. - - Text description of the unicode bindings, in a file coqide.bindings - one item per line, each item consists of: - - a leading backslahs - - a ascii word next to it - - a unicode word (or possibly a full sentence in-between doube-quotes, - the sentence may include spaces and \n tokens), - - optinally, an integer indicating the "priority" (lower is higher priority), - technically the length of the prefix that suffices to obtain this word. - Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda". - - \pi π - \lambda λ 3 - \lambdas λs 4 - \lake Ο 2 - \lemma "Lemma foo : x. Proof. Qed." 1 ---currently not supported by the parser - - - In case of equality between two candidates (same ascii word, or same - priorities for two words with similar prefix), the first binding is considered. - - - Note that if a same token is bound in several bindings file, - the one with the lowest priority number will be considered. - In case of same priority, the binding from the first loaded file is considered. -*) - -let unicode_bindings = ref [] - (* example unicode bindings table: - [ ("\\pi", "π", None); - ("\\lambdas", "λs", Some 4); - ("\\lambda", "λ", Some 3); - ("\\lake", "0", Some 2); - ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] *) - -let get_unicode_bindings () = - !unicode_bindings - -let process_unicode_bindings_file filename = - if not (Sys.file_exists filename) then begin - output_string stderr (Printf.sprintf "Error: unicode bindings file '%s' was not found.\n" filename); exit 1 - end; - let ch = open_in filename in - begin try while true do - let line = input_line ch in - begin try - let chline = Scanf.Scanning.from_string line in - let (key,value) = - Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in - let prio = - try Scanf.bscanf chline " %d" (fun x -> Some x) - with Scanf.Scan_failure _ | Failure _ | End_of_file -> None - in - unicode_bindings := (key,value,prio)::!unicode_bindings; - (* Note: storing bindings in reverse order, flipping is done later *) - Scanf.Scanning.close_in chline; - with End_of_file -> () end; - done with End_of_file -> () end; - close_in ch - -let load_unicode_bindings_files filenames = - let selected_filenames = ref [] in - let add f = - selected_filenames := f::!selected_filenames in - if filenames = [] then begin - (* If no argument is provided using [-unicode-bindings], - then use the default file and the local file, if it exists *) - begin match get_bindings_default_file() with - | Some f -> add f - | None -> output_string stderr (Printf.sprintf "Warning: the file ide/default.bindings was not found in %s.\n" (Envars.coqlib())) - (* TODO: flush stderr does not seem to eagerly display the output message *) - end; - begin match get_bindings_local_file() with - | Some f -> add f - | None -> () - end; - end else begin - (* If [-unicode-bindings] is used with a list of file, consider - these files in order, with a special treatment for the tokens - "default" and "local", which are replaced by the appropriate path. *) - let add_arg f = - match f with - | "default" -> - begin match get_bindings_default_file() with - | Some f -> add f - | None -> output_string stderr (Printf.sprintf "Error:the file ide/default.bindings was not found in %s.\n" (Envars.coqlib())); exit 1 - end - | "local" -> - begin match get_bindings_local_file() with - | Some f -> add f - | None -> output_string stderr (Printf.sprintf "Error: the local configuration file coqide.bindings was not found.\n"); exit 1 - end - | _ -> add f - in - List.iter add_arg filenames - end; - (* Files must be processed in order, to build the list of bindings - by iteratively consing entry to its head, the list being reversed - at the very end *) - let real_filenames = List.rev !selected_filenames in - List.iter process_unicode_bindings_file real_filenames; - unicode_bindings := List.rev !unicode_bindings - - (* For debugging the list of unicode files loaded: - List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames; - *) - (* For debugging the list of unicode bindings loaded: - let print_unicode_bindings () = - List.iter (fun (x,y,p) -> - Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) - !unicode_bindings; - prerr_newline() - *) - - (* TODO: known issue: the "~" in path of several arguments does - not seem to be correctly interpreted, e.g. - bin/coqide -unicode-bindings local,~/.config/coq/my.bindings & - Possible fix is to expand first to absolute paths. - *) diff --git a/ide/preferences.mli b/ide/preferences.mli index a75f1b3cec..2c505ad180 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -47,6 +47,10 @@ end val list_tags : unit -> tag preference Util.String.Map.t +val get_unicode_bindings_local_file : unit -> string option +val get_unicode_bindings_default_file : unit -> string option + + val cmd_coqtop : string option preference val cmd_coqc : string preference val cmd_make : string preference @@ -111,6 +115,3 @@ val stick : 'a preference -> (#GObj.widget as 'obj) -> ('a -> unit) -> unit val use_default_doc_url : string - -val get_unicode_bindings : unit -> (string * string * int option) list -val load_unicode_bindings_files : string list -> unit diff --git a/ide/unicode_bindings.ml b/ide/unicode_bindings.ml new file mode 100644 index 0000000000..e2f98302ea --- /dev/null +++ b/ide/unicode_bindings.ml @@ -0,0 +1,131 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* (x,y)) in + let prio = + try Scanf.bscanf chline " %d" (fun x -> Some x) + with Scanf.Scan_failure _ | Failure _ | End_of_file -> None + in + all_bindings := (key,value,prio)::!all_bindings; + (* Note: storing bindings in reverse order, flipping is done later *) + Scanf.Scanning.close_in chline; + with End_of_file -> () end; + done with End_of_file -> () end; + close_in ch + end + +let load_files filenames = + let selected_filenames = ref [] in + let add f = + selected_filenames := f::!selected_filenames in + let warn_default_not_found () = + Ideutils.warning (Printf.sprintf + "Warning: the file 'ide/default.bindings' was not found in %s." + (Envars.coqlib())) in + let warn_local_not_found () = + Ideutils.warning (Printf.sprintf + "Warning: the local configuration file 'coqide.bindings' was not found.") in + if filenames = [] then begin + (* If no argument is provided using [-unicode-bindings], + then use the default file and the local file, if it exists *) + begin match Preferences.get_unicode_bindings_default_file() with + | Some f -> add f + | None -> warn_default_not_found() + end; + begin match Preferences.get_unicode_bindings_local_file() with + | Some f -> add f + | None -> () + end; + end else begin + (* If [-unicode-bindings] is used with a list of file, consider + these files in order, with a special treatment for the tokens + "default" and "local", which are replaced by the appropriate path. *) + let add_arg f = + match f with + | "default" -> + begin match Preferences.get_unicode_bindings_default_file() with + | Some f -> add f + | None -> warn_default_not_found() + end + | "local" -> + begin match Preferences.get_unicode_bindings_local_file() with + | Some f -> add f + | None -> warn_local_not_found() + end + | _ -> add f + in + List.iter add_arg filenames + end; + (* Files must be processed in order, to build the list of bindings + by iteratively consing entry to its head, the list being reversed + at the very end *) + let real_filenames = List.rev !selected_filenames in + List.iter process_file real_filenames; + all_bindings := List.rev !all_bindings + (* For debugging the list of unicode files loaded: + List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames; *) + +(** Auxiliary function to test whether [s] is a prefix of [str]; + Note that there might be overlap with wg_Completion::is_substring *) + +let string_is_prefix s str = + let n = String.length s in + let m = String.length str in + if m < n + then false + else (s = String.sub str 0 n) + +let lookup prefix = + let max_priority = 100000000 in + let cur_word = ref None in + let cur_prio = ref (max_priority+1) in + let test_binding (key, word, prio_opt) = + let prio = + match prio_opt with + | None -> max_priority + | Some p -> p + in + if string_is_prefix prefix key && prio < !cur_prio then begin + cur_word := Some word; + cur_prio := prio; + end in + List.iter test_binding !all_bindings; + !cur_word + + +(* For debugging the list of unicode bindings loaded: + let print_unicode_bindings () = + List.iter (fun (x,y,p) -> + Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n)) + !all_bindings; + prerr_newline() +*) diff --git a/ide/unicode_bindings.mli b/ide/unicode_bindings.mli new file mode 100644 index 0000000000..5b38eeb920 --- /dev/null +++ b/ide/unicode_bindings.mli @@ -0,0 +1,48 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit + +(** [lookup] takes a prefix and returns the corresponding unicode value *) + +val lookup : string -> string option diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index efacaee577..a3f8aaab25 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -408,34 +408,6 @@ object (self) | _ -> () method apply_unicode_binding () = - let bindings = Preferences.get_unicode_bindings() in - (** Auxiliary function to test whether [s] is a prefix of [str]; - Note that there might be overlap with wg_Completion::is_substring *) - let string_is_prefix s str = - let n = String.length s in - let m = String.length str in - if m < n - then false - else (s = String.sub str 0 n) - in - (* Auxiliary function to perform the lookup for a binding *) - let lookup prefix = (* lookup : string -> string option *) - let max_priority = 100000000 in - let cur_word = ref None in - let cur_prio = ref (max_priority+1) in - let test_binding (key, word, prio_opt) = - let prio = - match prio_opt with - | None -> max_priority - | Some p -> p - in - if string_is_prefix prefix key && prio < !cur_prio then begin - cur_word := Some word; - cur_prio := prio; - end in - List.iter test_binding bindings; - !cur_word - in (** Auxiliary method to reach the beginning of line or the nearest space before the iterator. *) let rec get_line_start iter = @@ -458,7 +430,7 @@ object (self) in let prefix = backslash#get_text ~stop:insert in let word = - match lookup prefix with + match Unicode_bindings.lookup prefix with | None -> raise Abort | Some word -> word in @@ -466,6 +438,11 @@ object (self) if not was_deleted then raise Abort; word with Abort -> " " + (* Insert a space if no binding applies. This is to make sure that the user + gets some visual feedback that the keystroke was taken into account. + And also avoid slowing down users who press "Shift" for capitalizing the + first letter of a sentence just before typing the "Space" that comes in + front of that first letter. *) in let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in let _was_inserted = buffer#insert_interactive ~iter:insert2 word_to_insert in -- cgit v1.2.3 From 8ca754b1737adb4700609d43ef434a6d06c54ffe Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 28 Nov 2018 11:23:31 +0100 Subject: polishing documentation for coqide bindings, following @Zimmi48 comments --- doc/sphinx/practical-tools/coqide.rst | 36 +++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 44955412ce..6f48daf208 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -223,7 +223,7 @@ input Unicode characters. Displaying Unicode symbols -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~ You just need to define suitable notations as described in the chapter :ref:`syntaxextensionsandinterpretationscopes`. For example, to use the @@ -252,8 +252,8 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. -Defining an input method for non-ASCII symbols -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Bindings for input of Unicode symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ CoqIDE supports a builtin mechanism to input non-ASCII symbols. For example, to input ``π``, it suffices to type ``\pi`` then press the @@ -270,15 +270,17 @@ https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml Custom bindings may be added, as explained further on. -Remark: it remains possible to input non-ASCII symbols using system-wide -approaches independent of |CoqIDE|. +.. note:: + + It remains possible to input non-ASCII symbols using system-wide + approaches independent of |CoqIDE|. Adding custom bindings ~~~~~~~~~~~~~~~~~~~~~~ -To extend the default set of bindings, create a file named `coqide.bindings` -and place it in the same folder as `coqide.keys`. On Linux, this would be +To extend the default set of bindings, create a file named ``coqide.bindings`` +and place it in the same folder as ``coqide.keys``. On Linux, this would be the folder ``~/.config/coq``. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) @@ -307,15 +309,21 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. -Remark: if a filename other than the first one includes a "~" to refer -to the home directory, it won't be expanded properly. To work around that -issue, one should not use comas but instead repeat the flag, in the form: -``-unicode-bindings file1 .. -unicode-bindings fileN``. +.. remark:: + + If a filename other than the first one includes a "~" to refer + to the home directory, it won't be expanded properly. To work around that + issue, one should not use comas but instead repeat the flag, in the form: + ``-unicode-bindings file1 .. -unicode-bindings fileN``. + +.. note:: + + If two bindings for a same token both have the same priority value + (or both have no priority value set), then the binding considered is + the one from the file that comes first on the command line. -Remark: if two bindings for a same token both have the same priority value -(or both have no priority value set), then the binding considered is the -one from the file that comes first on the command line. +.. _character-encoding-saved-files: Character encoding for saved files ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 63abcb2c05ff1cab52fc6a4d3c0e93c91e8940e5 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 21 Nov 2018 09:19:34 +0000 Subject: [CoqIDE] dune rules for installing bindings --- ide/dune | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/ide/dune b/ide/dune index 3618e4f05d..f6414353f8 100644 --- a/ide/dune +++ b/ide/dune @@ -27,7 +27,7 @@ (library (name coqide_gui) (wrapped false) - (modules (:standard \ document fake_ide idetop coqide_main)) + (modules (:standard \ document fake_ide idetop coqide_main default_bindings_src)) (optional) (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) @@ -43,6 +43,16 @@ (modules coqide_main) (libraries coqide_gui)) +; Input-method bindings +(executable + (name default_bindings_src) + (modules default_bindings_src)) + +(rule + (targets default.bindings) + (deps (:gen ./default_bindings_src.exe)) + (action (run %{gen} %{targets}))) + ; FIXME: we should install those in share/coqide. We better do this ; once the make-based system has been phased out. (install @@ -50,6 +60,7 @@ (package coqide) (files (coq.png as coq/coq.png) + (default.bindings as coq/default.bindings) (coq_style.xml as coq/coq_style.xml) (coq.lang as coq/coq.lang) (coq-ssreflect.lang as coq/coq-ssreflect.lang))) -- cgit v1.2.3 From 67847789beede10420ab631d5d0f9c2cfe9db72d Mon Sep 17 00:00:00 2001 From: charguer Date: Mon, 11 Feb 2019 14:47:44 +0100 Subject: fix documentation issues, and add entry to change log --- CHANGES.md | 10 ++++++++++ doc/sphinx/practical-tools/coqide.rst | 21 ++++++++++++--------- 2 files changed, 22 insertions(+), 9 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 3e50a13e9e..c1755e9271 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -154,6 +154,16 @@ Tools - A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether conversion can use the VM. The default value is `yes`. +- CoqIDE now supports input for Unicode characters. For example, typing + "\alpha" then the "Shift+Space" will insert the greek letter alpha. + In fact, typing the prefix string "\a" is sufficient. + A larger number of default bindings are provided, following the latex + naming convention. Bindings can be customized, either globally, or on a + per-project basis, with the requirement is that keys must begin with a + backslash and contain no space character. Bindings may be assigned custom + priorities, so that prefixes resolve to the most convenient bindings. + The documentation pages for CoqIDE provides further details. + Standard Library - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 6f48daf208..97d86943fb 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -284,15 +284,18 @@ and place it in the same folder as ``coqide.keys``. On Linux, this would be the folder ``~/.config/coq``. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) -Here is an example configuration file: -``` -\par || -\pi π 1 -\le ≤ 1 -\lambda λ 2 -\lambdas λs -``` +.. example:: + + Here is an example configuration file: + + :: + + \par || + \pi π 1 + \le ≤ 1 + \lambda λ 2 + \lambdas λs Above, the priority number 1 on ``\pi`` indicates that the prefix ``\p`` should resolve to ``\pi``, and not to something else (e.g. ``\par``). @@ -309,7 +312,7 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. -.. remark:: +.. warning:: If a filename other than the first one includes a "~" to refer to the home directory, it won't be expanded properly. To work around that -- cgit v1.2.3 From 4298d6c15c425fd66e9673dee3fa27a3e9caafc9 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 5 Mar 2019 15:19:53 +0000 Subject: [ide] Address warning 50 --- ide/default_bindings_src.ml | 36 ++++++++++++++++++------------------ ide/wg_ScriptView.ml | 4 ++-- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/ide/default_bindings_src.ml b/ide/default_bindings_src.ml index 8d2291fcf9..85a635a50f 100644 --- a/ide/default_bindings_src.ml +++ b/ide/default_bindings_src.ml @@ -1517,7 +1517,7 @@ let bindings_set_1 = [ let bindings_set_2 = [ - (** Symbols *) + (* Symbols *) "\\!'", "¡"; "\\`", "‘"; "\\``", "“"; @@ -2046,7 +2046,7 @@ let bindings_set_2 = [ "\\xi", "ξ"; "\\zeta", "ζ"; - (** Double accent *) + (* Double accent *) "\\\"A", "Ä"; "\\\"E", "Ë"; "\\\"H", "Ḧ"; @@ -2067,7 +2067,7 @@ let bindings_set_2 = [ "\\\"x", "ẍ"; "\\\"y", "ÿ"; - (** Acute accent *) + (* Acute accent *) "\\'A", "Á"; "\\'C", "Ć"; "\\'E", "É"; @@ -2103,7 +2103,7 @@ let bindings_set_2 = [ "\\'y", "ý"; "\\'z", "ź"; - (** Doted accent *) + (* Doted accent *) "\\.A", "Ȧ"; "\\.B", "Ḃ"; "\\.C", "Ċ"; @@ -2224,7 +2224,7 @@ let bindings_set_2 = [ "\\dy", "ỵ"; "\\dz", "ẓ"; - (** Double dot accent *) + (* Double dot accent *) "\\ddots", "⋱"; "\\ddotA", "Ä"; "\\ddotE", "Ë"; @@ -2246,7 +2246,7 @@ let bindings_set_2 = [ "\\ddotx", "ẍ"; "\\ddoty", "ÿ"; - (** Breve accent *) + (* Breve accent *) "\\breveA", "Ă"; "\\breveE", "Ĕ"; "\\breveG", "Ğ"; @@ -2272,7 +2272,7 @@ let bindings_set_2 = [ "\\uo", "ŏ"; "\\uu", "ŭ"; - (** Check accent *) + (* Check accent *) "\\checkA", "Ǎ"; "\\checkC", "Č"; "\\checkD", "Ď"; @@ -2310,7 +2310,7 @@ let bindings_set_2 = [ "\\vt", "ť"; "\\vz", "ž"; - (** Bar accent *) + (* Bar accent *) "\\=A", "Ā"; "\\=E", "Ē"; "\\=G", "Ḡ"; @@ -2342,7 +2342,7 @@ let bindings_set_2 = [ "\\baru", "ū"; "\\bary", "ȳ"; - (** Hat acccent *) + (* Hat acccent *) "\\^A", "Â"; "\\^C", "Ĉ"; "\\^E", "Ê"; @@ -2370,7 +2370,7 @@ let bindings_set_2 = [ "\\^y", "ŷ"; "\\^z", "ẑ"; - (** Backquote acccent *) + (* Backquote acccent *) "\\`A", "À"; "\\`E", "È"; "\\`I", "Ì"; @@ -2388,7 +2388,7 @@ let bindings_set_2 = [ "\\`w", "ẁ"; "\\`y", "ỳ"; - (** Tiled acccent *) + (* Tiled acccent *) "\\~A", "Ā"; "\\~E", "Ẽ"; "\\~I", "Ĩ"; @@ -2404,7 +2404,7 @@ let bindings_set_2 = [ "\\~u", "ũ"; "\\~y", "ỹ"; - (** textrt font *) + (* textrt font *) "\\textrtaild", "ɖ"; "\\textrtaill", "ɭ"; "\\textrtailn", "ɳ"; @@ -2413,7 +2413,7 @@ let bindings_set_2 = [ "\\textrtailt", "ʈ"; "\\textrtailz", "ʐ"; - (** textsc font *) + (* textsc font *) "\\textscb", "ʙ"; "\\textscg", "ɢ"; "\\textsch", "ʜ"; @@ -2427,7 +2427,7 @@ let bindings_set_2 = [ "\\textscriptv", "ʋ"; "\\textscy", "ʏ"; - (** bb font *) + (* bb font *) "\\bb0", "𝟘"; "\\bb1", "𝟙"; "\\bb2", "𝟚"; @@ -2491,7 +2491,7 @@ let bindings_set_2 = [ "\\bby", "𝕪"; "\\bbz", "𝕫"; - (** cal font *) + (* cal font *) "\\calA", "𝒜"; "\\calB", "ℬ"; "\\calC", "𝒞"; @@ -2545,7 +2545,7 @@ let bindings_set_2 = [ "\\caly", "𝓎"; "\\calz", "𝓏"; - (** frak font *) + (* frak font *) "\\frakA", "𝔄"; "\\frakB", "𝔅"; "\\frakC", "ℭ"; @@ -2599,7 +2599,7 @@ let bindings_set_2 = [ "\\fraky", "𝔶"; "\\frakz", "𝔷"; - (** Exponent *) + (* Exponent *) "\\^(", "⁽"; "\\^)", "⁾"; "\\^+", "⁺"; @@ -2670,7 +2670,7 @@ let bindings_set_2 = [ "\\^y", "ʸ"; "\\^z", "ᶻ"; - (** Subscript *) + (* Subscript *) "\\_(", "₍"; "\\_)", "₎"; "\\_+", "₊"; diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index a3f8aaab25..bfa9d6e0c5 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -408,13 +408,13 @@ object (self) | _ -> () method apply_unicode_binding () = - (** Auxiliary method to reach the beginning of line or the + (* Auxiliary method to reach the beginning of line or the nearest space before the iterator. *) let rec get_line_start iter = if iter#starts_line || Glib.Unichar.isspace iter#char then iter else get_line_start iter#backward_char in - (** Main action *) + (* Main action *) let buffer = self#buffer in let insert = buffer#get_iter `INSERT in let insert_mark = buffer#create_mark ~left_gravity:false insert in -- cgit v1.2.3