[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