Emacs 24.4.1 中的下标未正确显示
Subscripts in Emacs 24.4.1 not showing up properly
我正在做一个使用 unicode 下标 k(“\_k”)的作业。但是,我没有得到下标 k,而是得到了这个:
![][1]
仍然可以使用数字和一些字母的下标,但不能使用 'k'。
我最初遇到了 emacs 24.3 的问题,然后被告知更新到 24.4。问题仍然存在。
有没有其他人遇到过这个问题并找到了解决方案?
我 运行 在 Mac 上使用 Emacs v.24.4.1
提前致谢
编辑
这是我的 .emacs 文件:
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
(set-default-font "-apple-DejaVu_Sans-medium-normal-normal-*-*-*-*-*-p-0-iso10646-1")
; Change Control-c Control-, and Control-c Control-. in Agda mode
; so they show the normalized rather than the "simplified" goals
(defun agda2-normalized-goal-and-context ()
(interactive)
(agda2-goal-and-context '(3)))
(defun agda2-normalized-goal-and-context-and-inferred ()
(interactive)
(agda2-goal-and-context-and-inferred '(3)))
(eval-after-load "agda2-mode"
'(progn
(define-key agda2-mode-map (kbd "C-c C-,")
'agda2-normalized-goal-and-context)
(define-key agda2-mode-map (kbd "C-c C-.")
'agda2-normalized-goal-and-context-and-inferred)))
; This defines backslash commands for some extra symbols.
(eval-after-load "quail/latin-ltx"
'(mapc (lambda (pair)
(quail-defrule (car pair) (cadr pair) "TeX"))
'( ("\bb" "") ("\bl" "") ("\bs" "")
("\bt" "") ("\bv" "") ("\cv" "⋎")
("\comp" "∘") ("\m" "↦") ("\om" "ω"))))
; This sets the Control-c Control-k shortcut to
; describe the character under your cursor.
(global-set-key "\C-c\C-k" 'describe-char)
(custom-set-variables
'(agda2-include-dirs
(quote ("." "/Users/dylanthiemann/Dropbox/University of Iowa/2nd Senior Year/Spring 2015/PLC/ial")))
)
这部分代码来自 Agda:
module bool-kleene-thms where
open import bool
open import bool-kleene
open import eq
&&ₖ-idem : ∀ (b : ₖ) → b &&ₖ b ≡ b
&&ₖ-idem b = {!!}
tt-&&ₖ : ∀ (b : ₖ) → tt &&ₖ b ≡ b
tt-&&ₖ b = {!!}
||ₖ-idem : ∀ (b : ₖ) → b ||ₖ b ≡ b
||ₖ-idem b = {!!}
||ₖ-tt : ∀ (b : ₖ) → b ||ₖ tt ≡ tt
||ₖ-tt b = {!!}
||ₖ-ff : ∀ (b : ₖ) → b ||ₖ ff ≡ b
||ₖ-ff b = {!!}
编辑 2
Ctrl-u Ctrl-x =
对受影响角色的结果:
position: 91 of 830 (11%), column: 2
character: ₖ (displayed as ₖ) (codepoint 8342, #o20226, #x2096)
preferred charset: unicode (Unicode (ISO10646))
code point in charset: 0x2096
script: symbol
syntax: w which means: word
category: .:Base, L:Left-to-right (strong)
to input: type "\_k" with Agda input method
buffer code: #xE2 #x82 #x96
file code: #xE2 #x82 #x96 (encoded by coding system utf-8-unix)
display: terminal code #xE2 #x82 #x96
我需要安装新字体...我使用了这个 http://dejavu-fonts.org/wiki/Download 然后使用 Font Books 安装。然后问题就解决了!
我正在做一个使用 unicode 下标 k(“\_k”)的作业。但是,我没有得到下标 k,而是得到了这个:
![][1]
仍然可以使用数字和一些字母的下标,但不能使用 'k'。
我最初遇到了 emacs 24.3 的问题,然后被告知更新到 24.4。问题仍然存在。
有没有其他人遇到过这个问题并找到了解决方案?
我 运行 在 Mac 上使用 Emacs v.24.4.1
提前致谢
编辑
这是我的 .emacs 文件:
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
(set-default-font "-apple-DejaVu_Sans-medium-normal-normal-*-*-*-*-*-p-0-iso10646-1")
; Change Control-c Control-, and Control-c Control-. in Agda mode
; so they show the normalized rather than the "simplified" goals
(defun agda2-normalized-goal-and-context ()
(interactive)
(agda2-goal-and-context '(3)))
(defun agda2-normalized-goal-and-context-and-inferred ()
(interactive)
(agda2-goal-and-context-and-inferred '(3)))
(eval-after-load "agda2-mode"
'(progn
(define-key agda2-mode-map (kbd "C-c C-,")
'agda2-normalized-goal-and-context)
(define-key agda2-mode-map (kbd "C-c C-.")
'agda2-normalized-goal-and-context-and-inferred)))
; This defines backslash commands for some extra symbols.
(eval-after-load "quail/latin-ltx"
'(mapc (lambda (pair)
(quail-defrule (car pair) (cadr pair) "TeX"))
'( ("\bb" "") ("\bl" "") ("\bs" "")
("\bt" "") ("\bv" "") ("\cv" "⋎")
("\comp" "∘") ("\m" "↦") ("\om" "ω"))))
; This sets the Control-c Control-k shortcut to
; describe the character under your cursor.
(global-set-key "\C-c\C-k" 'describe-char)
(custom-set-variables
'(agda2-include-dirs
(quote ("." "/Users/dylanthiemann/Dropbox/University of Iowa/2nd Senior Year/Spring 2015/PLC/ial")))
)
这部分代码来自 Agda:
module bool-kleene-thms where
open import bool
open import bool-kleene
open import eq
&&ₖ-idem : ∀ (b : ₖ) → b &&ₖ b ≡ b
&&ₖ-idem b = {!!}
tt-&&ₖ : ∀ (b : ₖ) → tt &&ₖ b ≡ b
tt-&&ₖ b = {!!}
||ₖ-idem : ∀ (b : ₖ) → b ||ₖ b ≡ b
||ₖ-idem b = {!!}
||ₖ-tt : ∀ (b : ₖ) → b ||ₖ tt ≡ tt
||ₖ-tt b = {!!}
||ₖ-ff : ∀ (b : ₖ) → b ||ₖ ff ≡ b
||ₖ-ff b = {!!}
编辑 2
Ctrl-u Ctrl-x =
对受影响角色的结果:
position: 91 of 830 (11%), column: 2
character: ₖ (displayed as ₖ) (codepoint 8342, #o20226, #x2096)
preferred charset: unicode (Unicode (ISO10646))
code point in charset: 0x2096
script: symbol
syntax: w which means: word
category: .:Base, L:Left-to-right (strong)
to input: type "\_k" with Agda input method
buffer code: #xE2 #x82 #x96
file code: #xE2 #x82 #x96 (encoded by coding system utf-8-unix)
display: terminal code #xE2 #x82 #x96
我需要安装新字体...我使用了这个 http://dejavu-fonts.org/wiki/Download 然后使用 Font Books 安装。然后问题就解决了!