+ public static int font_size() {
+ return font_size;
+ }
+
+ static void set_fonts() {
+ }
+
+ public static void set_font_size(int new_font_size) {
+ font_size = new_font_size;
+ synchronized (preferences) {
+ preferences.putInt(fontSizePreference, font_size);
+ flush_preferences();
+ Altos.set_fonts(font_size);
+ for (AltosFontListener l : font_listeners)
+ l.font_size_changed(font_size);
+ }
+ }
+
+ public static void register_font_listener(AltosFontListener l) {
+ synchronized (preferences) {
+ font_listeners.add(l);
+ }
+ }
+
+ public static void unregister_font_listener(AltosFontListener l) {
+ synchronized (preferences) {
+ font_listeners.remove(l);
+ }
+ }
+