bool changeArmColour = false);
extern void wxDoChangeFont(WXWidget widget, const wxFont& font);
extern void wxGetTextExtent(WXDisplay* display, const wxFont& font,
bool changeArmColour = false);
extern void wxDoChangeFont(WXWidget widget, const wxFont& font);
extern void wxGetTextExtent(WXDisplay* display, const wxFont& font,