[isabelle-dev] x-symbols

David Aspinall David.Aspinall at ed.ac.uk
Tue Aug 25 20:02:40 CEST 2009

Lawrence Paulson wrote:
> Does anybody know what would cause the symbols that look like this? It 
> is the latest version of proof general running under GNU Emacs 22.2.1

Nobody else came running so I'll answer...

First of all: everyone will have a *much* better experience with Emacs 
23.x if you can find/build a version.  It's what persuaded me Emacs was 
worth sticking with.  I wish they would release it properly.  Some Linux 
distributions (e.g. Ubuntu) are distributing it as a package now 

Supposing you have to stick with Emacs 22.2:

This effect is caused by using a font which does not have glyphs in the 
Unicode positions for the tokens.   You can select a better font to 
improve matters, try:

   Tokens -> Make fontsets

and then

    Options -> Set font/fontset

and try the possibilities on the "Fontset" submenu. On the Linux I'm 
using right now, I get a better result with the fontset 
"standard:16-dot-medium" than I do with the custom pgXXX fontsets 
created by the first menu command.  Not sure why, it wasn't the case 
when I wrote all the fontset support mess a year ago.

I thought I had documented this somewhere but can't find it now, must admit.

  - David

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

More information about the isabelle-dev mailing list