[Agda] unicode input

Martin Escardo m.escardo at cs.bham.ac.uk
Wed May 18 13:42:52 CEST 2016


When I type \MIV I get a bold V, as I should.

But then after type-checking the file with "Load" (Ctrl-C Ctrl-L), I get 
a box with microscopic

    01D
    47D

inside.

When I do "Kill and restart Agda", I see bold V again.

When I cat the file in the command line, I see the bold V and all 
unicode characters as I intend.

So I seem to have the fonts available.

This happens to many other unicode characters, but not all.

My emacs is 24.3.1 under ubuntu 14.04.

Any ideas?

Thanks,
Martin
PS 1. This doesn't happen in a laptop running ubuntu 16.06 with emacs 
24.5.1.

PS 2. In both machines, when the offending characters are displayed 
correctly, still we have a problem that a blank line is displayed above 
the character's line, and also below.


More information about the Agda mailing list