<div dir="ltr">Hi Martin,<div><br></div><div>Nice to meet you at the UniMath workshop. I tried this out and the character displays fine for me; I'm using a Mac, GNU Emacs, and whatever the default font is (seems to be a Mac font).</div><div><br></div><div>One thing to try is would be to do M-x describe-char on both instances of 𝓟; it should show which font is being used to render it.  In both cases I get:</div><div><div>              display: by this font (glyph code)</div><div>    mac-ct:-*-STIXGeneral-normal-normal-normal-*-16-*-*-*-p-0-iso10646-1 (#x9D6)</div></div><div><br></div><div>Of course why emacs would be using a different font for each buffer would be a different question....</div><div><br></div><div>John</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Dec 22, 2017 at 12:33 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
I want to use the powerset symbol, which is \MCP (calligraphic capital<br>
P).<br>
<br>
If I do agda-input-show-translations, then I get to see this symbol<br>
properly rendered, saying that it should be typed as \MCP.<br>
<br>
However, when I use \MCP in an agda file, the symbol is not rendered<br>
(by the same emacs session) and I instead see a square with a matrix<br>
of hexadecimal numbers inside it.<br>
<br>
Let me try it here to see what the message is displayed like: 𝓟.<br>
<br>
I have<br>
<br>
   (set-fontset-font "fontset-default" 'unicode "DejaVu Sans")<br>
<br>
in my .emacs as suggested here in this list some time ago (I think by<br>
Paolo Capriotti), which works for many symbols, but not this.<br>
<br>
Why can emacs display it in the agda-input-show-translations buffer,<br>
but not in my agda buffer? Any clues?<br>
<br>
Thanks,<br>
Martin<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>