Save fonts in XBoard settings file per boardSize

Save fonts in XBoard settings file per boardSize

Each -boardSize now can have its own font specified in the settings file
(and thus by a command-line option, although it would in general not be
very useful to specify a font for a size other than the selected). E.g.
a prefix "size33:" to the font name will apply it only to -size 33.
An unspecified-size font option (not normally in the settings file) will
always prevail over a font option specific for the current size.
A font of some size must have been used or specified in order to be
saved.