X-Symbol on Mac OS X, natively

There are at least two nice native ports of GNU Emacs for Mac OS X: Carbon Emacs and Aquamacs.

These work well with Proof General except for the lack of support for X-Symbol. The problem is that X-Symbol contains some custom fonts which were built for the X font server machinery, in bdf format. These fonts contain mathematical symbols, derived from TeX fonts set at different sizes and at a fixed width.

It would be good if these fonts could be made available in a format understood by Mac OS X, and then in turn used inside a native Emacs port. It looks as if nobody has done this yet, so I gave it a try. Unfortunately I wasn't completely successful, but someone with a bit more time/determination could probably finish things off. One of the main problems is working around pecularities of font formats and encodings to get the fonts understood both by Mac OS X and by Carbon Emacs (whose font support is still in development).

There are three basic ways to go: most basic to the eventual best, which is to use Unicode fonts instead of the old X-Symbol ones. The improved ways would also work with the future xft Emacs on Linux.

Bitmap conversion: embed bdf files into a format understood by Font Book

First attempt was with ufond (part of fondu package):

 cd ProofGeneral/x-symbol/etc/fonts
 ufond -dfont xsymb0*.bdf

This produces a file XSymb0.fam.dfont which gets silently ignored by Fontbook. It's possibly re-encoded into Mac Latin as well, but this can maybe be stopped by setting the script code:

 ufond -dfont -script 32 xsymb0*.bdf

The file can be loaded into fontforge and saved again from there in different formats (also experimenting with encodings). I got better results doing that than any of the command line utilities I tried (although fontforge is scriptable, so once you know what works, you can write the code to do it).

The aim is to get a result where Emacs recognises the font in its current hacky XFLD-emulating way:

( x-list-fonts "-apple-xsymb0-*")

Should return a list of fonts at the available pixel sizes and with a useful encoding. (You need to restart Emacs after each addition/removal in Font Book).

In practice with this first mechanism I could only see pixel sizes of 0 in the font list (standing for a scalable font) and most usually encoding iso10646, UCS. I'm not sure that the encoding iso10646 is useful. The reason seems to be (I'm guessing) is that Emacs gets scared if a character set doesn't seem to contain any ASCII characters, so when making a fontset it searches for a nearby font with ASCII characters and adds them to the fontset. I managed to get much further with an incantation like this:

(create-fontset-from-fontset-spec
 "-apple-xsymb0-medium-r-normal--14-*-*-*-*-*-fontset-xsymb0,
 ascii:-apple-xsymb0-medium-r-normal--14-*-*-*-*-*-iso10646-1,
latin-iso8859-1:-apple-xsymb0-medium-r-normal--14-*-*-*-*-*-iso10646-1")

You can then select the resulting fontset xsymb0 from the Emacs menu to check that it works: you see gibberish with some mathematical symbols, great! The rendering system will even resize these bitmap fonts to sizes that they weren't included in. The lisp files need a little bit of reworking to load the right fonts (changes in x-symbol-vars.el) and tweak the calls to new-fontset (in x-symbol-emacs.el or x-symbol-mule.el) to get around the problem mentioned, but this seems possible to do, perhaps using some switches to preserve the normal behaviour.

to be completed: or please try to do this yourself and share the results!

Start from the source: make outline and anti-aliasing versions of the X-Symbol fonts

The disadvantage of the above route, even if it can be made to work smoothly, is that the bitmap fonts are still rendered without anti-aliasing and look ugly compared with the beautiful rendering of the native Emacs ports. I'm not sure if there is a way to fix that. In any case, we're still stuck with a fixed range of low-resolution sizes and interpolation between them.

On the x-symbol pages at sourceforge, Christoph Wedler made available a download called x-symbol-additional-fonts. What this actually contains is most of the machinery for generating the x-symb0 and x-symb1 fonts distributed with X-Symbol. The symbols are generated using fontforge (previously known as Pfaedit). This works by automatically tracing the output of metafont (for single glyphs taken directly from TeX fonts) and sometimes tracing gif files derived from the output TeX (for symbols which are constructed by TeX by composing several glyphs from characters in TeX fonts). Then the resulting outline font is used to generate bdf fonts in a range of sizes. You can see what a huge project X-Symbol must have been!

(Incidently: the mechanism of tracing and hinting from the metafont sources has been highly tuned since X-Symbol was written, cm-super is a complete set of outline fonts generated in this way; the other sets of outline fonts, such as Bluesky's, have had manual tuning).

Unfortunately Christoph didn't include any outline versions of the original fonts in his distributions. Regenerating them approximately using this source package is possible --- in fact it can be improved upon by importing most of the symbols from existing Type 1 fonts instead of retracing. I have done this (with some painstaking renaming of glyphs), to get Type 1 versions of XSymb0 and XSymb1. These can be used to make fonts which can be loaded into Mac OS X that scale perfectly.

to be completed: the fonts I made have a few problems which I may fix one day; please ask me for the sources if you are interested

The future: use Unicode fonts

X-Symbol is something of a dinosaur: it was invented when Emacs didn't always come with mechanisms for dealing with different character encodings, so some of the machinery of Mule, for example, is duplicated. Hopefully in future someone will write a nice LaTeX package that uses modern Emacs mechanisms like Norman Walsh's Unicode for XML package to achieve semi-Wysiwyg easily, and make use of the existing and upcoming symbol-rich Unicode fonts.

In the meantime, it would be useful to have a backwards compatibility mechanism to use Unicode fonts with X-Symbol so that we can continue to use its nice interface (e.g. handy symbol grid, categorization of characters, nice keyboard shortcuts, etc).

I've also attempted this and got reasonably far. The main work is in constructing a mapping of X-Symbol charsym names into Unicode positions (which I have done via the Unicode names). The files aren't quite complete but I hope to post something here (or add to a development version of PG) at some point. At the moment, the main problem is that some useful symbols seem to be missing from the Mac Unicode fonts (e.g. long arrows). These could maybe be synthesised by combining several glyphs. The problem after that would be to deal with sub/superscripts: I'm not sure whether the Emacs display engine is able to offset characters to give them different baselines. X-Symbol solves this problem by generating yet more fonts which have shifted positions. Developing a new U-Symbol package would make a great project for someone!

Unicode patch for X-Symbol: to be completed

An appeal for semi-Wysiwyg

By the way, an alternative to the X-Symbol mechanism would be to have something like preview-latex in proof script buffers, for displaying presentation views of complex formulae alongside their input forms. In the wonderful Eclipse interface we could popup a presentation view of a formulae when the mouse hovers. This would fit in neatly with our ideas for authoring proof scripts, and also work well with the input/output disparity in Isabelle. However, preview-latex doesn't go far enough (look at all those \Delta tokens).

But does X-Symbol go far enough? You might ask why anyone would want to bother with the X-Symbol mode of editing at all. The modern way would surely to be have an "equation editor" which constructs formulae e.g. in MathML, for input to the proof assistant either directly in the presentation format (which requires reinterpretation) or in some underlying content format. It's the editing and display of the content format that we want to support here. The typing of complex formulae directly in a compact and understandable linear, logical markup like TeX is widespread by mathematicians and computer scientists, at least, and seems unlikely to go away anytime soon. Displaying and typing symbols like \Sigma directly as ∑ makes formulae even more compact, and their logical structure can still be directly understood.

Probably people who prefer to write their papers in Microsoft Word than struggle with LaTeX will prefer editing in a presentation-oriented view, but ultimately I believe we need to have both mechanisms available, to suit different people and different purposes. But there's no need to spell out the names of "unusual" letters and symbols.

[David Aspinall, Oct 2006]