Problem with wide unicode characters in emacs 23.3

[Generic Isabelle user]

In Emacs23.3, when replacing tokens like \<Longrightarrow>, they are not recognized as wide characters, i.e. emacs thinks, they are still as wide as a normal character. This leads to problems, as emacs then overprints parts of the inserted character.

It does work when inserting the unicode symbol itself (i.e. not using the token-support) - so it does not look like an emacs problem per se.

Even more interesting, it also works flawlessly with emacs 23.2.

This was tested with ProofGeneral-4.1pre101216-p1 and ProofGeneral-4.1pre110601

[Generic Isabelle user]

Ok ... it works with emacs-23.3 under Debian but not under Gentoo. And from the patches applied to either version, I cannot see what makes the difference *sigh*

[Generic Isabelle user]

Ok ... this indeed seemed to be a problem with emacs. That it worked under certain circumstances was pure luck (for instance it didn't work in a fresh Debian but in a fresh Fedora ...).

Anyways: There is a commit in emacs/trunk (and emacs/emacs-23) that fixes this issue: ​http://bzr.savannah.gnu.org/lh/emacs/emacs-23/revision/100586 (found via bisecting)

I'll attach the patch that can be applied to get a working Emacs-23.3 for future reference.

[David Aspinall]

Thanks for the (impressive) investigation and recording here!

There are a few other tickets (search for keyword "emacsbug") if you can fathom the Emacs display engine C code...

[David Aspinall]

Note: unfortunately Ubuntu 12.04 and perhaps other recent Linux versions may still include a broken Emacs (23.3), but I've noticed that simply installing STIX fonts may be a workaround anyway for this problem (the bad display seems to happen when the system lacks the right characters). On Ubuntu, simply try:

  sudo apt-get install fonts-stix

Changing the font selected to Deja Vu Sans Mono also seems to repair things, so I have reverted this to be the default font in PG 4.2 as it works out-of-the-box.