extern void init_fontmenu(Widget tool);
extern void setup_fontmenu(void);