DeeTee
DeeTee

Reputation: 707

Subscripts in Emacs 24.4.1 not showing up properly

I'm working on an assignment that used the unicode subscript k ("\_k"). However, instead of getting the subscripted k, I get this:

![][1]

The can still use subscripts with numbers and some letters, but not with 'k'.

I initially had the issue with emacs 24.3, and then was told to update to 24.4. The issue still persisted.

Has anyone else had this issue and found a solution?

I'm running on a Mac with Emacs v.24.4.1

Thanks in advance

EDIT

Here is my .emacs file:

(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")))
 )

And the bit of code is from 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 = {!!}

Edit 2

Results of Ctrl-u Ctrl-x = on affected character:

             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

Upvotes: 5

Views: 796

Answers (1)

DeeTee
DeeTee

Reputation: 707

I needed to install new fonts... I used this http://dejavu-fonts.org/wiki/Download and then installed using Font Books. The issue was then resolved!

Upvotes: 6

Related Questions