add vim digraphs to emacs
This commit is contained in:
Julin S
parent
17f4d5ef18
commit
28e1589857
61
emacs/.emacs
61
emacs/.emacs
|
|
@ -25,6 +25,10 @@
|
|||
|
||||
;; Set default encoding as UTF-8
|
||||
(set-terminal-coding-system 'utf-8)
|
||||
(set-keyboard-coding-system 'utf-8)
|
||||
(set-selection-coding-system 'utf-8)
|
||||
(setq locale-coding-system 'utf-8)
|
||||
(prefer-coding-system 'utf-8)
|
||||
|
||||
|
||||
; Don't show welcome screen every time
|
||||
|
|
@ -60,6 +64,7 @@
|
|||
|
||||
;; shortcuts only for proofgeneral mode
|
||||
(eval-after-load "proof-script"
|
||||
; Show goal and in vertical splits
|
||||
'(setq proof-three-window-mode-policy 'hybrid))
|
||||
|
||||
|
||||
|
|
@ -81,3 +86,59 @@
|
|||
|
||||
; Disable automatic indentation
|
||||
(setq electric-indent-mode nil)
|
||||
|
||||
|
||||
; Vim digraphs
|
||||
(load-file "~/.config/emacs/digraphs.el")
|
||||
|
||||
|
||||
; (defun get-buffer-contents (buffer)
|
||||
; (with-current-buffer buffer
|
||||
; (save-restriction
|
||||
; (widen)
|
||||
; (buffer-substring-no-properties (point-min) (point-max)))))
|
||||
;
|
||||
; (defun coq-insert-output-as-comment (buffer description)
|
||||
; ; can be bound to a key combination
|
||||
; (interactive)
|
||||
;
|
||||
; ; save current cursor position
|
||||
; (save-excursion
|
||||
;
|
||||
; ; go to end of current line
|
||||
; (end-of-line)
|
||||
;
|
||||
; ; insert text
|
||||
; (insert
|
||||
; (concat
|
||||
; "\n(*\n#+BEGIN_OUTPUT ("
|
||||
; description
|
||||
; ")\n\n"
|
||||
; (get-buffer-contents buffer)
|
||||
; "\n#+END_OUTPUT ("
|
||||
; description
|
||||
; ")\n*)\n"))))
|
||||
;
|
||||
;
|
||||
; (eval-after-load "proof-script"
|
||||
; '(progn
|
||||
; ; change key combination for undo previous line
|
||||
; (define-key proof-mode-map
|
||||
; (kbd "C- C-u") 'proof-prf)
|
||||
;
|
||||
; (define-key proof-mode-map
|
||||
; (kbd "C- C-p") 'proof-undo-last-successful-command)
|
||||
;
|
||||
; ; Add key combinations to display Info and Goal
|
||||
; (define-key proof-mode-map
|
||||
; (kbd "C-c i")
|
||||
; (lambda ()
|
||||
; (interactive)
|
||||
; (coq-insert-output-as-comment "*response*" "Info")))
|
||||
;
|
||||
; (define-key proof-mode-map
|
||||
; (kbd "C-c j")
|
||||
; (lambda ()
|
||||
; (interactive)
|
||||
; (coq-insert-output-as-comment "*goals*" "Goal")))
|
||||
; ))
|
||||
|
|
|
|||
|
|
@ -1,2 +1,3 @@
|
|||
Located at `~`.
|
||||
- `.emacs`: `~/`
|
||||
- `digraphs.el`: `~/.config/emacs/digraphs.el`
|
||||
|
||||
|
|
|
|||
201
emacs/digraphs.el
Normal file
201
emacs/digraphs.el
Normal file
|
|
@ -0,0 +1,201 @@
|
|||
;; Vim digraphs
|
||||
; https://mullikine.github.io/posts/adding-new-digraphs-to-vim-and-evil/
|
||||
|
||||
;((?) . ?-) ?\x2209) ; ∉
|
||||
|
||||
(setq evil-digraphs-table-user '(
|
||||
((?R ?s) . ?\x20a8) ; ₨
|
||||
((?r ?s) . ?\x20b9) ; ₹ (INR)
|
||||
((?^ ?0) . ?\x2070) ; ⁰ (duplicate of 0S)
|
||||
((?^ ?1) . ?\xb9) ; ¹ (duplicate of 1S)
|
||||
((?^ ?2) . ?\xb2) ; ² (duplicate of 2S)
|
||||
((?^ ?3) . ?\xb3) ; ³ (duplicate of 3S)
|
||||
((?^ ?4) . ?\x2074) ; ⁴ (duplicate of 4S)
|
||||
((?^ ?5) . ?\x2075) ; ⁵ (duplicate of 5S)
|
||||
((?^ ?6) . ?\x2076) ; ⁶ (duplicate of 6S)
|
||||
((?^ ?7) . ?\x2077) ; ⁷ (duplicate of 7S)
|
||||
((?^ ?8) . ?\x2078) ; ⁸ (duplicate of 8S)
|
||||
((?^ ?9) . ?\x2079) ; ⁹ (duplicate of 9S)
|
||||
((?^ ?a) . ?\x1d43) ; ᵃ
|
||||
((?^ ?b) . ?\x1d47) ; ᵇ
|
||||
((?^ ?c) . ?\x1d9c) ; ᶜ
|
||||
((?^ ?d) . ?\x1d48) ; ᵈ
|
||||
((?^ ?e) . ?\x1d49) ; ᵉ
|
||||
((?^ ?f) . ?\x1da0) ; ᶠ
|
||||
((?^ ?g) . ?\x1d4d) ; ᵍ
|
||||
((?^ ?h) . ?\x2b0) ; ʰ
|
||||
((?^ ?i) . ?\x2071) ; ⁱ
|
||||
((?^ ?j) . ?\x2b2) ; ʲ
|
||||
((?^ ?k) . ?\x1d4f) ; ᵏ
|
||||
((?^ ?l) . ?\x2e1) ; ˡ
|
||||
((?^ ?m) . ?\x1d50) ; ᵐ
|
||||
((?^ ?n) . ?\x207f) ; ⁿ
|
||||
((?^ ?o) . ?\x1d52) ; ᵒ
|
||||
((?^ ?p) . ?\x1d56) ; ᵖ
|
||||
((?^ ?r) . ?\x2b3) ; ʳ
|
||||
((?^ ?s) . ?\x2e2) ; ˢ
|
||||
((?^ ?t) . ?\x1d57) ; ᵗ
|
||||
((?^ ?u) . ?\x1d58) ; ᵘ
|
||||
((?^ ?v) . ?\x1d5b) ; ᵛ
|
||||
((?^ ?w) . ?\x2b7) ; ʷ
|
||||
((?^ ?x) . ?\x2e3) ; ˣ
|
||||
((?^ ?y) . ?\x2b8) ; ʸ
|
||||
((?^ ?z) . ?\x1dbb) ; ᶻ
|
||||
((?^ ?A) . ?\x1d2c) ; ᴬ
|
||||
((?^ ?B) . ?\x1d2e) ; ᴮ
|
||||
((?^ ?D) . ?\x1d30) ; ᴰ
|
||||
((?^ ?E) . ?\x1d31) ; ᴱ
|
||||
((?^ ?G) . ?\x1d33) ; ᴳ
|
||||
((?^ ?H) . ?\x1d34) ; ᴴ
|
||||
((?^ ?I) . ?\x1d35) ; ᴵ
|
||||
((?^ ?J) . ?\x1d36) ; ᴶ
|
||||
((?^ ?K) . ?\x1d37) ; ᴷ
|
||||
((?^ ?L) . ?\x1d38) ; ᴸ
|
||||
((?^ ?M) . ?\x1d39) ; ᴹ
|
||||
((?^ ?N) . ?\x1d3a) ; ᴺ
|
||||
((?^ ?O) . ?\x1d3c) ; ᴼ
|
||||
((?^ ?P) . ?\x1d3e) ; ᴾ
|
||||
((?^ ?R) . ?\x1d3f) ; ᴿ
|
||||
((?^ ?T) . ?\x1d40) ; ᵀ
|
||||
((?^ ?U) . ?\x1d41) ; ᵁ
|
||||
((?^ ?V) . ?\x2c7d) ; ⱽ
|
||||
((?^ ?W) . ?\x1d42) ; ᵂ
|
||||
((?^ ?+) . ?\x207a) ; ⁺ (duplicate of +S)
|
||||
((?^ ?-) . ?\x207b) ; ⁻ (duplicate of -S)
|
||||
((?^ ?=) . ?\x207c) ; ⁼
|
||||
((?^ ?() . ?\x207d) ; ⁽
|
||||
((?^ ?)) . ?\x207e) ; ⁾
|
||||
((?_ ?0) . ?\x2080) ; ₀ (duplicate of 0s)
|
||||
((?_ ?1) . ?\x2081) ; ₁ (duplicate of 1s)
|
||||
((?_ ?2) . ?\x2082) ; ₂ (duplicate of 2s)
|
||||
((?_ ?3) . ?\x2083) ; ₃ (duplicate of 3s)
|
||||
((?_ ?4) . ?\x2084) ; ₄ (duplicate of 4s)
|
||||
((?_ ?5) . ?\x2085) ; ₅ (duplicate of 5s)
|
||||
((?_ ?6) . ?\x2086) ; ₆ (duplicate of 6s)
|
||||
((?_ ?7) . ?\x2087) ; ₇ (duplicate of 7s)
|
||||
((?_ ?8) . ?\x2088) ; ₈ (duplicate of 8s)
|
||||
((?_ ?9) . ?\x2089) ; ₉ (duplicate of 9s)
|
||||
((?_ ?a) . ?\x2090) ; ₐ
|
||||
((?_ ?e) . ?\x2091) ; ₑ
|
||||
((?_ ?h) . ?\x2095) ; ₕ
|
||||
((?_ ?i) . ?\x1d62) ; ᵢ
|
||||
((?_ ?j) . ?\x2c7c) ; ⱼ
|
||||
((?_ ?k) . ?\x2096) ; ₖ
|
||||
((?_ ?l) . ?\x2097) ; ₗ
|
||||
((?_ ?m) . ?\x2098) ; ₘ
|
||||
((?_ ?n) . ?\x2099) ; ₙ
|
||||
((?_ ?o) . ?\x2092) ; ₒ
|
||||
((?_ ?p) . ?\x209a) ; ₚ
|
||||
((?_ ?r) . ?\x1d63) ; ᵣ
|
||||
((?_ ?s) . ?\x209b) ; ₛ
|
||||
((?_ ?t) . ?\x209c) ; ₜ
|
||||
((?_ ?u) . ?\x1d64) ; ᵤ
|
||||
((?_ ?v) . ?\x1d65) ; ᵥ
|
||||
((?_ ?x) . ?\x2093) ; ₓ
|
||||
((?_ ?+) . ?\x208a) ; ₊ (duplicate of +s)
|
||||
((?_ ?-) . ?\x208b) ; ₋ (duplicate of -s)
|
||||
((?_ ?=) . ?\x208c) ; ₌
|
||||
((?_ ?() . ?\x208d) ; ₍
|
||||
((?_ ?)) . ?\x208e) ; ₎
|
||||
((?/ ?A) . ?\x1d434) ; 𝐴
|
||||
((?/ ?B) . ?\x1d435) ; 𝐵
|
||||
((?/ ?C) . ?\x1d436) ; 𝐶
|
||||
((?/ ?D) . ?\x1d437) ; 𝐷
|
||||
((?/ ?E) . ?\x1d438) ; 𝐸
|
||||
((?/ ?F) . ?\x1d439) ; 𝐹
|
||||
((?/ ?G) . ?\x1d43a) ; 𝐺
|
||||
((?/ ?H) . ?\x1d43b) ; 𝐻
|
||||
((?/ ?I) . ?\x1d43c) ; 𝐼
|
||||
((?/ ?J) . ?\x1d43d) ; 𝐽
|
||||
((?/ ?K) . ?\x1d43e) ; 𝐾
|
||||
((?/ ?L) . ?\x1d43f) ; 𝐿
|
||||
((?/ ?M) . ?\x1d440) ; 𝑀
|
||||
((?/ ?N) . ?\x1d441) ; 𝑁
|
||||
((?/ ?O) . ?\x1d442) ; 𝑂
|
||||
((?/ ?P) . ?\x1d443) ; 𝑃
|
||||
((?/ ?Q) . ?\x1d444) ; 𝑄
|
||||
((?/ ?R) . ?\x1d445) ; 𝑅
|
||||
((?/ ?S) . ?\x1d446) ; 𝑆
|
||||
((?/ ?T) . ?\x1d447) ; 𝑇
|
||||
((?/ ?U) . ?\x1d448) ; 𝑈
|
||||
((?/ ?V) . ?\x1d449) ; 𝑉
|
||||
((?/ ?W) . ?\x1d44a) ; 𝑊
|
||||
((?/ ?X) . ?\x1d44b) ; 𝑋
|
||||
((?/ ?Y) . ?\x1d44c) ; 𝑌
|
||||
((?/ ?Z) . ?\x1d44d) ; 𝑍
|
||||
((?/ ?a) . ?\x1d44e) ; 𝑎
|
||||
((?/ ?b) . ?\x1d44f) ; 𝑏
|
||||
((?/ ?c) . ?\x1d450) ; 𝑐
|
||||
((?/ ?d) . ?\x1d451) ; 𝑑
|
||||
((?/ ?e) . ?\x1d452) ; 𝑒
|
||||
((?/ ?f) . ?\x1d453) ; 𝑓 (overriding ⁄: Fraction slash)
|
||||
((?/ ?g) . ?\x1d454) ; 𝑔
|
||||
((?/ ?h) . ?\x210e) ; ℎ (using Planck constant)
|
||||
((?/ ?i) . ?\x1d456) ; 𝑖
|
||||
((?/ ?j) . ?\x1d457) ; 𝑗
|
||||
((?/ ?k) . ?\x1d458) ; 𝑘
|
||||
((?/ ?l) . ?\x1d459) ; 𝑙
|
||||
((?/ ?m) . ?\x1d45a) ; 𝑚
|
||||
((?/ ?n) . ?\x1d45b) ; 𝑛
|
||||
((?/ ?o) . ?\x1d45c) ; 𝑜
|
||||
((?/ ?p) . ?\x1d45d) ; 𝑝
|
||||
((?/ ?q) . ?\x1d45e) ; 𝑞
|
||||
((?/ ?r) . ?\x1d45f) ; 𝑟
|
||||
((?/ ?s) . ?\x1d460) ; 𝑠
|
||||
((?/ ?t) . ?\x1d461) ; 𝑡
|
||||
((?/ ?u) . ?\x1d462) ; 𝑢
|
||||
((?/ ?v) . ?\x1d463) ; 𝑣
|
||||
((?/ ?w) . ?\x1d464) ; 𝑤
|
||||
((?/ ?x) . ?\x1d465) ; 𝑥
|
||||
((?/ ?y) . ?\x1d466) ; 𝑦
|
||||
((?/ ?z) . ?\x1d467) ; 𝑧
|
||||
((?N ?N) . ?\x2115) ; ℕ: Set of natural numbers
|
||||
((?R ?R) . ?\x211d) ; ℝ: Set of real numbers
|
||||
((?Z ?Z) . ?\x2124) ; ℤ: Set of integers
|
||||
((?C ?C) . ?\x2102) ; ℂ: Set of complex numbers (overriding ~T: Cancel character)
|
||||
((?Q ?Q) . ?\x211a) ; ℚ: Set of rational numbers
|
||||
((?B ?B) . ?\x1d539) ; 𝔹: Set of Booleans (overriding ¦)
|
||||
((?e ?e) . ?\x212f) ; ℯ: Euler's number ≅ 2.71828
|
||||
((?p ?h) . ?\x2135) ; ℵ : Aleph number (in addition to א (A+))
|
||||
((?e ?l) . ?\x2113) ; ℓ
|
||||
((?T ?N) . ?\x2204) ; ∄ (Since ∃ is TE)
|
||||
((?n ?<) . ?\x219a) ; ↚ (Since ← is <-)
|
||||
((?n ?>) . ?\x219b) ; ↛ (Since → is ->)
|
||||
((?p ?r) . ?\x22a2) ; ⊢
|
||||
((?M ?O) . ?\x22a8) ; ⊨
|
||||
((?n ?p) . ?\x22ac) ; ⊬
|
||||
((?N ?M) . ?\x22ad) ; ⊭
|
||||
((?b ?x) . ?\x25a1) ; □ (duplicate of OS)
|
||||
((?d ?m) . ?\x25c7) ; ◇ (duplicate of Dw)
|
||||
((?! ?3) . ?\x2262) ; ≢ (because ≡ is `digr =3`)
|
||||
((?m ?p) . ?\x21a6) ; ↦: maps to
|
||||
((?F ?F) . ?\x27d8) ; ⊥ (like False) (overriding : Form feed)
|
||||
((?T ?T) . ?\x27d9) ; ⊤ (like True) (duplicate of -T)
|
||||
((?d ?t) . ?\x22c5) ; ⋅ ('small dot')
|
||||
((?D ?T) . ?\x2022) ; • ('big dot') (overriding ^?: DELETE character)
|
||||
((?r ?2) . ?\x221a) ; √ (square root) (duplicate of RT)
|
||||
((?r ?3) . ?\x221b) ; ∛ (cube root)
|
||||
((?r ?4) . ?\x221c) ; ∜ (fourth root)
|
||||
((?p ?p) . ?\x27c2) ; ⟂ (perpendicular to)
|
||||
((?l ?l) . ?\x2016) ; ‖ (parallel to)
|
||||
((?k ?t) . ?\x27e9) ; ⟩ (ket symbol)
|
||||
((?~ ?~) . ?\x336) ; strikethrough text overlay
|
||||
((?A ?~) . ?\xc3) ; Ã (duplicate of 'A?')
|
||||
((?E ?~) . ?\x1ebc) ; Ẽ (duplicate of 'E?')
|
||||
((?I ?~) . ?\x128) ; Ĩ (duplicate of 'I?')
|
||||
((?N ?~) . ?\xd1) ; Ñ (duplicate of 'N?')
|
||||
((?O ?~) . ?\xd5) ; Õ (duplicate of 'O?')
|
||||
((?U ?~) . ?\x168) ; Ũ (duplicate of 'U?')
|
||||
((?V ?~) . ?\x1e7c) ; Ṽ (duplicate of 'V?')
|
||||
((?Y ?~) . ?\x1ef8) ; Ỹ (duplicate of 'Y?')
|
||||
((?a ?~) . ?\xe3) ; ã (duplicate of 'a?')
|
||||
((?e ?~) . ?\x1ebd) ; ẽ (duplicate of 'e?')
|
||||
((?i ?~) . ?\x129) ; ĩ (duplicate of 'i?')
|
||||
((?n ?~) . ?\xf1) ; ñ (duplicate of 'n?')
|
||||
((?o ?~) . ?\xf5) ; õ (duplicate of 'o?')
|
||||
((?u ?~) . ?\x169) ; ũ (duplicate of 'u?')
|
||||
((?v ?~) . ?\x1e7d) ; ṽ (duplicate of 'v?')
|
||||
((?y ?~) . ?\x1ef9) ; ỹ (duplicate of 'y?')
|
||||
((?4 ?4) . ?\x25b) ; ɛ
|
||||
((?c ?c) . ?\x254) ; ɔ
|
||||
))
|
||||
|
|
@ -12,7 +12,18 @@ source ~/.vimrc
|
|||
|
||||
se nohls
|
||||
|
||||
" Allow pasting to system clipboard
|
||||
" Thanks to: ShougoShougo#neovim
|
||||
if has('unnamedplus')
|
||||
set clipboard& clipboard+=unnamedplus
|
||||
else
|
||||
set clipboard& clipboard+=unnamed
|
||||
endif
|
||||
|
||||
" Coqtail stuff
|
||||
let @i=":CoqJumpToEnd | call append('.', ['(* -- AUTO OUTPUT (Info) --'] + getbufline(b:coqtail_panel_bufs['info'], 1, '$') + ['*)'])
"
|
||||
|
||||
let @g=":CoqJumpToEnd | call append('.', ['(* -- AUTO OUTPUT (Goal) --'] + getbufline(b:coqtail_panel_bufs['goal'], 1, '$') + ['*)'])
"
|
||||
|
||||
" Emacs proofgeneral-like shortcuts for coqtail
|
||||
noremap <C-n> :CoqNext<CR>hh " next line. Dunno why cursor advaces horizontally 2 chars.
|
||||
noremap <C-p> :CoqUndo<CR>hh " undo last line
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user