- 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);
- }
- }