[Agda] List of fonts required for Emacs mode?

[David Banas]

Oh, I see. So, you’ve left the agda2-fontset-name variable at its default value: nil, then?

I guess I went too deep and should’ve taken the simpler path; D’oh! ;-)

Thanks!
-db


> On Jul 29, 2020, at 8:42 AM, András Kovács <puttamalac at gmail.com> wrote:
> 
> I've only used "options->set default font" in the emacs menu bar, that sets the font globally.
> 
> David Banas <capn.freako at gmail.com <mailto:capn.freako at gmail.com>> ezt írta (időpont: 2020. júl. 29., Sze, 15:55):
> Okay, thanks.
> 
> Do you, then, set the value of the agda2-fontset-name variable to <DejaVu/Mononoki proper font name>, as opposed to "fontset-agda2"?
> 
> -db
> 
> 
> On Wed, Jul 29, 2020 at 2:47 AM András Kovács <puttamalac at gmail.com <mailto:puttamalac at gmail.com>> wrote:
> Hi,
> 
> Strictly speaking, there isn't a required font, rather, people tend to use monospace fonts with good unicode support. 
> I personally use DejaVu Sans Mono. The PLFA book recommends Mononoki <https://plfa.github.io/GettingStarted/#using-mononoki-in-emacs>. 
> 
> David Banas <capn.freako at gmail.com <mailto:capn.freako at gmail.com>> ezt írta (időpont: 2020. júl. 29., Sze, 1:26):
> Hi,
> 
> Would someone be so kind as to post the list of required fonts for the Agda Emacs mode?
> I can't seem to find them in the documentation.
> 
> Thanks,
> -db
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200729/36d991a0/attachment.html>