Implement (clock-)font handling in GTK

Implement (clock-)font handling in GTK

The options -clockFont, -coordFont and -messageFont are activated,
and supposed to have string values like "Sans Bold 12". The default
values have the point size as 'wild-card' %d, however "Sans Bold %d",
and are expanded by a printf with the point size taken from the defaults
table. The expanded versions are saved back into the settings file,
prefixed with a size tag, as usual.
 So far -clockFont is the only font that is actually applied while
writing.
 The 'clock kludge' was interfering with the initial sizing, as for some
sizes the initial clock-widget height happened to be equal to the final
height. It was therefore abandoned, and we seem to be able to live without
it.
 Sizes smaller than 49 were dominated (for 8-wide boards) by the menu bar.
Therefore tinyLayout now uses single-letter menu labels.