[Agda] Font questions again

[John Leo]

Hi Martin,

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).

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:
              display: by this font (glyph code)
    mac-ct:-*-STIXGeneral-normal-normal-normal-*-16-*-*-*-p-0-iso10646-1
(#x9D6)

Of course why emacs would be using a different font for each buffer would
be a different question....

John

On Fri, Dec 22, 2017 at 12:33 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
> I want to use the powerset symbol, which is \MCP (calligraphic capital
> P).
>
> If I do agda-input-show-translations, then I get to see this symbol
> properly rendered, saying that it should be typed as \MCP.
>
> However, when I use \MCP in an agda file, the symbol is not rendered
> (by the same emacs session) and I instead see a square with a matrix
> of hexadecimal numbers inside it.
>
> Let me try it here to see what the message is displayed like: 𝓟.
>
> I have
>
>    (set-fontset-font "fontset-default" 'unicode "DejaVu Sans")
>
> in my .emacs as suggested here in this list some time ago (I think by
> Paolo Capriotti), which works for many symbols, but not this.
>
> Why can emacs display it in the agda-input-show-translations buffer,
> but not in my agda buffer? Any clues?
>
> Thanks,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171222/a3ac0b66/attachment.html>