From 57314d18609cb7a0949c9b80f457ff22a7fdfac0 Mon Sep 17 00:00:00 2001
From: Silvus <s8bnpete@stud.uni-saarland.de>
Date: Mon, 22 Aug 2022 18:58:55 +0200
Subject: [PATCH] Added UltiSnips as an alternative way of inserting unicode
 characters in Vim

---
 docs/editor.md | 537 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 537 insertions(+)

diff --git a/docs/editor.md b/docs/editor.md
index 5ba7e03da..cd9b19684 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -688,3 +688,540 @@ let g:unicode_map = {
   \ "_x"        :   "â‚“",
 \ }
 ```
+
+
+Alternatively, you can use snippets using [UltiSnips](https://github.com/SirVer/ultisnips).
+
+Install it with your favorite plugin manager, and register a completion key in your configuration:
+```
+let g:UltiSnipsExpandTrigger="<c-l>"
+```
+To insert a unicode character, type its trigger word, such as `\forall`, and then press `<c-l>` while still in insert mode.
+
+To register most common unicode characters, put the following file either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim:
+```
+snippet \forall "" i
+∀
+endsnippet
+snippet \exists "" i
+∃
+endsnippet
+snippet \lam "" i
+λ
+endsnippet
+snippet \not "" i
+¬
+endsnippet
+snippet \lor "" i
+∨
+endsnippet
+snippet \land "" i
+∧
+endsnippet
+snippet \/ "" i
+∨
+endsnippet
+snippet /\ "" i
+∧
+endsnippet
+snippet \rightarrow "" i
+→
+endsnippet
+snippet \implies "" i
+→
+endsnippet
+snippet -> "" i
+→
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet <-> "" i
+↔
+endsnippet
+snippet \<- "" i
+←
+endsnippet
+snippet \cong "" i
+≡
+endsnippet
+snippet \== "" i
+≡
+endsnippet
+snippet \/== "" i
+≢
+endsnippet
+snippet \neq "" i
+≠
+endsnippet
+snippet /= "" i
+≠
+endsnippet
+snippet \less "" i
+≤
+endsnippet
+snippet \le "" i
+≤
+endsnippet
+snippet <= "" i
+≤
+endsnippet
+snippet \in "" i
+∈
+endsnippet
+snippet \notin "" i
+∉
+endsnippet
+snippet \cup "" i
+∪
+endsnippet
+snippet \cap "" i
+∩
+endsnippet
+snippet \setminus "" i
+∖
+endsnippet
+snippet \subset "" i
+⊂
+endsnippet
+snippet \subseteq "" i
+⊆
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \notsubseteq "" i
+⊈
+endsnippet
+snippet \meet "" i
+⊓
+endsnippet
+snippet \join "" i
+⊔
+endsnippet
+snippet \true "" i
+⊤
+endsnippet
+snippet \top "" i
+⊤
+endsnippet
+snippet \false "" i
+⊥
+endsnippet
+snippet \bottom "" i
+⊥
+endsnippet
+snippet \vdash "" i
+⊢
+endsnippet
+snippet \dashv "" i
+⊣
+endsnippet
+snippet \vDash "" i
+⊨
+endsnippet
+snippet \Vdash
+⊩
+endsnippet
+snippet \infty "" i
+∞
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \prf "" i
+↾
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+snippet \mapsto "" i
+↦
+endsnippet
+snippet \hookrightarrow "" i
+↪
+endsnippet
+snippet \up "" i
+↑
+endsnippet
+snippet \uparrow "" i
+↑
+endsnippet
+
+snippet \fun "" i
+λ
+endsnippet
+snippet \mult "" i
+â‹…
+endsnippet
+snippet \ent "" i
+⊢
+endsnippet
+snippet \valid "" i
+✓
+endsnippet
+snippet \diamond "" i
+â—‡
+endsnippet
+snippet \box "" i
+â–¡
+endsnippet
+snippet \bbox "" i
+â– 
+endsnippet
+snippet \eval "" i
+â–·
+endsnippet
+snippet \rhd "" i
+â–·
+endsnippet
+snippet \later "" i
+â–·
+endsnippet
+snippet \pred "" i
+φ
+endsnippet
+snippet \and "" i
+∧
+endsnippet
+snippet \or "" i
+∨
+endsnippet
+snippet \circ "" i
+∘
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \ccomp "" i
+â—Ž
+endsnippet
+snippet \pound "" i
+£
+endsnippet
+snippet \all "" i
+∀
+endsnippet
+snippet \ex "" i
+∃
+endsnippet
+snippet \to "" i
+→
+endsnippet
+snippet \ast "" i
+∗
+endsnippet
+snippet \sep "" i
+∗
+endsnippet
+snippet \ulc "" i
+⌜
+endsnippet
+snippet \urc "" i
+⌝
+endsnippet
+snippet \lc "" i
+⌜
+endsnippet
+snippet \rc "" i
+⌝
+endsnippet
+snippet \Lc "" i
+⎡
+endsnippet
+snippet \Rc "" i
+⎤
+endsnippet
+snippet \varnothing "" i
+∅
+endsnippet
+snippet \empty "" i
+∅
+endsnippet
+snippet \Lam "" i
+Λ
+endsnippet
+snippet \Sig "" i
+Σ
+endsnippet
+snippet \- "" i
+∖
+endsnippet
+snippet \aa "" i
+●
+endsnippet
+snippet \af "" i
+â—¯
+endsnippet
+snippet \auth "" i
+●
+endsnippet
+snippet \frag "" i
+â—¯
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet \gname "" i
+γ
+endsnippet
+snippet \incl "" i
+≼
+endsnippet
+snippet \latert "" i
+â–¶
+endsnippet
+snippet \update "" i
+⇝
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+
+
+snippet ^^+ "" i
+⁺
+endsnippet
+snippet __+ "" i
+â‚Š
+endsnippet
+snippet ^^- "" i
+⁻
+endsnippet
+snippet __0 "" i
+â‚€
+endsnippet
+snippet __1 "" i
+₁
+endsnippet
+snippet __2 "" i
+â‚‚
+endsnippet
+snippet __3 "" i
+₃
+endsnippet
+snippet __4 "" i
+â‚„
+endsnippet
+snippet __5 "" i
+â‚…
+endsnippet
+snippet __6 "" i
+₆
+endsnippet
+snippet __7 "" i
+₇
+endsnippet
+snippet __8 "" i
+₈
+endsnippet
+snippet __9 "" i
+₉
+endsnippet
+
+snippet __a "" i
+ₐ
+endsnippet
+snippet __e "" i
+â‚‘
+endsnippet
+snippet __h "" i
+â‚•
+endsnippet
+snippet __i "" i
+áµ¢
+endsnippet
+snippet __k "" i
+â‚–
+endsnippet
+snippet __l "" i
+â‚—
+endsnippet
+snippet __m "" i
+ₘ
+endsnippet
+snippet __n "" i
+â‚™
+endsnippet
+snippet __o "" i
+â‚’
+endsnippet
+snippet __p "" i
+â‚š
+endsnippet
+snippet __r "" i
+áµ£
+endsnippet
+snippet __s "" i
+â‚›
+endsnippet
+snippet __t "" i
+ₜ
+endsnippet
+snippet __u "" i
+ᵤ
+endsnippet
+snippet __v "" i
+áµ¥
+endsnippet
+snippet __x "" i
+â‚“
+endsnippet
+
+snippet \Alpha "" i
+Α
+endsnippet
+snippet \alpha "" i
+α
+endsnippet
+snippet \Beta "" i
+Î’
+endsnippet
+snippet \beta "" i
+β
+endsnippet
+snippet \Gamma "" i
+Γ
+endsnippet
+snippet \gamma "" i
+γ
+endsnippet
+snippet \Delta "" i
+Δ
+endsnippet
+snippet \delta "" i
+δ
+endsnippet
+snippet \Epsilon "" i
+Ε
+endsnippet
+snippet \epsilon "" i
+ε
+endsnippet
+snippet \Zeta "" i
+Ζ
+endsnippet
+snippet \zeta "" i
+ζ
+endsnippet
+snippet \Eta "" i
+Η
+endsnippet
+snippet \eta "" i
+η
+endsnippet
+snippet \Theta "" i
+Θ
+endsnippet
+snippet \theta "" i
+θ
+endsnippet
+snippet \Iota "" i
+Ι
+endsnippet
+snippet \iota "" i
+ι
+endsnippet
+snippet \Kappa "" i
+Κ
+endsnippet
+snippet \kappa "" i
+κ
+endsnippet
+snippet \Lamda "" i
+Λ
+endsnippet
+snippet \lamda "" i
+λ
+endsnippet
+snippet \Lambda "" i
+Λ
+endsnippet
+snippet \lambda "" i
+λ
+endsnippet
+snippet \Mu "" i
+Μ
+endsnippet
+snippet \mu "" i
+μ
+endsnippet
+snippet \Nu "" i
+Ν
+endsnippet
+snippet \nu "" i
+ν
+endsnippet
+snippet \Xi "" i
+Ξ
+endsnippet
+snippet \xi "" i
+ξ
+endsnippet
+snippet \Omicron "" i
+Ο
+endsnippet
+snippet \omicron "" i
+ο
+endsnippet
+snippet \Pi "" i
+Π
+endsnippet
+snippet \pi "" i
+Ï€
+endsnippet
+snippet \Rho "" i
+Ρ
+endsnippet
+snippet \rho "" i
+ρ
+endsnippet
+snippet \Sigma "" i
+Σ
+endsnippet
+snippet \sigma "" i
+σ
+endsnippet
+snippet \Tau "" i
+Τ
+endsnippet
+snippet \tau "" i
+Ï„
+endsnippet
+snippet \Upsilon "" i
+Î¥
+endsnippet
+snippet \upsilon "" i
+Ï…
+endsnippet
+snippet \Phi "" i
+Φ
+endsnippet
+snippet \phi "" i
+Ï•
+endsnippet
+snippet \varphi "" i
+φ
+endsnippet
+snippet \Chi "" i
+Χ
+endsnippet
+snippet \chi "" i
+χ
+endsnippet
+snippet \Psi "" i
+Ψ
+endsnippet
+snippet \psi "" i
+ψ
+endsnippet
+snippet \Omega "" i
+Ω
+endsnippet
+snippet \omega "" i
+ω
+endsnippet
+```
-- 
GitLab