mailing-list for TeXmacs Users

[David Allouche <address@hidden>]

On Sunday 16 December 2001 23:41,  Sebastian C. B. Sauer wrote:
> Is there an easy way of changing the menu bar font? I would much prefer
> having a sans-serif font for the menu.

It depends on what is an easy way for you.

I had a look at TeXmacs source, and it seems that user interface widgets are 
created using the default font defined in the display class.

So you will have to change this font. A quick look in TeXmacs initialization 
files has not revealed any command used to set the default font, so I assume 
you have to change the font defined in the source.

The default font is defined in src/Window/X/x_font.gen.cc in the 
x_display_rep::default_font method (line 199).

Here you will find the following statement:
return tex_ec_font (this, "ecrm", 11, 300);

Just change "ecrm" to "ecss" to have TeXmacs use a sans-serif font. Of course 
you will have to recompile an reinstall TeXmacs, but that's a very simple 
business if you are used to the standard GNU installation system, also known 
as "./configure && make && make install".

Changing the default font of the display will not affect the default font 
used in documents.

I consider this to be easy, but I understand some people are not 
confortable with tweaking source and recompiling software.

> so long,

And thanks for all the fish.