+ 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);
+ }
+ }
+
+ public static void set_look_and_feel(String new_look_and_feel) {
+ look_and_feel = new_look_and_feel;
+ try {
+ UIManager.setLookAndFeel(look_and_feel);
+ } catch (Exception e) {
+ }
+ synchronized(preferences) {
+ preferences.put(lookAndFeelPreference, look_and_feel);
+ flush_preferences();
+ for (AltosUIListener l : ui_listeners)
+ l.ui_changed(look_and_feel);
+ }
+ }
+
+ public static String look_and_feel() {
+ return look_and_feel;
+ }
+
+ public static void register_ui_listener(AltosUIListener l) {
+ synchronized(preferences) {
+ ui_listeners.add(l);
+ }
+ }
+
+ public static void unregister_ui_listener(AltosUIListener l) {
+ synchronized (preferences) {
+ ui_listeners.remove(l);
+ }
+ }