+if (! isset($default_fontset)) $default_fontset=SMPREF_NONE;
+$chosen_fontset = getPref($data_dir, $username, 'chosen_fontset', $default_fontset);
+if (! isset($default_fontsize)) $default_fontsize=SMPREF_NONE;
+$chosen_fontsize = getPref($data_dir, $username, 'chosen_fontsize', $default_fontsize);
+