{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/873","labels_url":"https://api.github.com/repos/leanprover/lean/issues/873/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/873/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/873/events","html_url":"https://github.com/leanprover/lean/issues/873","id":117000331,"number":873,"title":"Some symbols not being displayed correctly","user":{"login":"bbentzen","id":15263295,"avatar_url":"https://avatars.githubusercontent.com/u/15263295?v=3","gravatar_id":"","url":"https://api.github.com/users/bbentzen","html_url":"https://github.com/bbentzen","followers_url":"https://api.github.com/users/bbentzen/followers","following_url":"https://api.github.com/users/bbentzen/following{/other_user}","gists_url":"https://api.github.com/users/bbentzen/gists{/gist_id}","starred_url":"https://api.github.com/users/bbentzen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bbentzen/subscriptions","organizations_url":"https://api.github.com/users/bbentzen/orgs","repos_url":"https://api.github.com/users/bbentzen/repos","events_url":"https://api.github.com/users/bbentzen/events{/privacy}","received_events_url":"https://api.github.com/users/bbentzen/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"milestone":null,"comments":18,"created_at":"2015-11-15T16:04:52Z","updated_at":"2015-11-23T18:00:56Z","closed_at":null,"body":"I wonder why some characters are not being displayed correctly in my emacs (v.24.5.1), as the image below shows:\r\n![test](https://cloud.githubusercontent.com/assets/15263295/11169421/0f4e4b92-8bf2-11e5-81d9-ee71852d3d04.png)\r\nIt seems emacs displays them as some sort of character code instead.\r\n\r\nFor reference, the symbols in the picture are the following:\r\n\r\n```javascript\r\ndefinition whisker_right [unfold 7] {p q : x = y} (h : p = q) (r : y = z) : p ⬝ r = q ⬝ r :=\r\n  h ◾ idp\r\n```\r\n\r\n```javascript\r\n‒ – — ‘ ’ ‚ „ † ‡ • … ‰ ﹠ ＆ ·\r\n  ¤ ¢ £ € ¥ ¦ § ¶ © ® ™\r\n¼ ½ ¾\r\n“” ‹› «» 〔〕 〈〉 《》 「」 『』 【】〖〗\r\nΑ Β Γ Δ Ε Ζ Η Θ Ι Κ Λ Μ Ν Ξ Ο Π Ρ Σ Τ Υ Φ Χ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ ο π ρ ς σ τ υ φ χ ψ ω\r\nℬ ℭ ℰ ℱ ℋ ℳ ℘ ℛ ℨ\r\nℯ ℊ ℌ ℐ ℑ ℒ ℓ ℴ ℜ\r\nℂ ℕ ℙ ℚ ℝ ℤ ℍ\r\nℵ ⅆ ⅇ ⅈ ⅉ ∅\r\nÅ ב ג ד\r\nƒ µ ø Ø Þ ß ϑ ϒ ϖ Ϝ ϝ\r\n° ‾ ⁄\r\nsuperscript ⁰ ¹ ² ³ ⁴ ⁵ ⁶ ⁷ ⁸ ⁹ ⁺ ⁻ ⁼ ⁽ ⁾ ⁿ ⁱ\r\nsubscript ₀ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉ ₊ ₋ ₌ ₍ ₎ ₐ ₑ ₒ ₓ ₔ ᵢ ⱼ ᵥ\r\n← → ↔ ↑ ↓ ↖ ↘ ↚ ↛ ↮\r\n↤ ↦ ⇤ ⇥\r\n⇐ ⇒ ⇔ ⇑ ⇓\r\n⇍ ⇏ ⇎\r\n⟵ ⟶ ⟷ ⟸ ⟹ ⟺\r\n∀ ∃ ∴\r\n¬ ∧ ∨ ⊻ ⊼ ⊽ ⊥\r\n∈ ∉ ∋\r\n⊕ ⊗ ⋅ ⨯\r\n∝ ∞\r\n⌈ ⌉ ⌊ ⌋\r\n⌘ ⌚ ⌛ ⏏ ␣ ⌤ ⌥ ⌧ ⌫ ⌶ ⎋ ⎗ ⎘ ⎙ ✂ ✄ ✉ ✍ ⌨ ⏎ ↩ ↵ ↶ ↷ ↹ ⇄ ⇧ ⇞ ⇟\r\n⓪ ① ② ③ ④ ⑤ ⑥ ⑦ ⑧ ⑨\r\n■ □ ▲ △ ▶ ▷ ▼ ▽ ◀ ◁ ◆ ◇ ◊ ○ ● ★ ☹ ☺\r\n☉ ☼ ☽ ☾ ☿ ♀ ♁ ♂ ♃ ♄ ♅ ♆ ♇ ☄\r\n♠ ♣ ♥ ♦ ♩ ♪ ♫ ♬ ♭ ♮ ♯\r\n```\r\n\r\nI tried a lot but I can't figure out what is causing emacs to behave like this.."},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/159012626","html_url":"https://github.com/leanprover/lean/issues/873#issuecomment-159012626","issue_url":"https://api.github.com/repos/leanprover/lean/issues/873","id":159012626,"user":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"created_at":"2015-11-23T18:00:56Z","updated_at":"2015-11-23T18:00:56Z","body":"@bbentzen \r\n\r\nPlease try `http` instead of `https`, that is, please have the following in your `.emacs` file:\r\n\r\n```elisp\r\n(add-to-list 'package-archives\r\n'(\"melpa\" . \"http://melpa.org/packages/\"))\r\n```\r\n\r\nThis should help. Reference: https://github.com/milkypostman/melpa/issues/2109"}}