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(-) (limited to 'ide') 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 (limited to 'ide') 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(-) (limited to 'ide') 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(-) (limited to 'ide') 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 --- ide/default.bindings | 1156 ----------------- ide/default_bindings_src.ml | 2899 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 2899 insertions(+), 1156 deletions(-) delete mode 100644 ide/default.bindings create mode 100644 ide/default_bindings_src.ml (limited to 'ide') 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(-) (limited to 'ide') 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 --- ide/preferences.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'ide') 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 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(-) (limited to 'ide') 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 --- 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 +++---------- 7 files changed, 193 insertions(+), 156 deletions(-) create mode 100644 ide/unicode_bindings.ml create mode 100644 ide/unicode_bindings.mli (limited to 'ide') 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 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(-) (limited to 'ide') 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 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(-) (limited to 'ide') 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