altosdroid: Add text size selection

[fw/altos] / altosdroid / app / src / main / java / org / altusmetrum / AltosDroid / AltosDroidPreferences.java

diff --git a/altosdroid/app/src/main/java/org/altusmetrum/AltosDroid/AltosDroidPreferences.java b/altosdroid/app/src/main/java/org/altusmetrum/AltosDroid/AltosDroidPreferences.java
index 6ec9e4d19b867802c38af3b257989f2b55441b73..f23955685389d43ed93bf4e12adf626676a375e2 100644 (file)
--- a/altosdroid/app/src/main/java/org/altusmetrum/AltosDroid/AltosDroidPreferences.java
+++ b/altosdroid/app/src/main/java/org/altusmetrum/AltosDroid/AltosDroidPreferences.java
@@ -28,6 +28,15 @@ public class AltosDroidPreferences extends AltosPreferences {
        final static String activeDeviceAddressPreference = "ACTIVE-DEVICE-ADDRESS";
        final static String activeDeviceNamePreference = "ACTIVE-DEVICE-NAME";
 
+       public static final int font_size_small = 0;
+       public static final int font_size_medium = 1;
+       public static final int font_size_large = 2;
+       public static final int font_size_extra = 3;
+
+       final static String fontSizePreference = "FONT-SIZE";
+
+       static int font_size = font_size_medium;
+
        static DeviceAddress    active_device_address;
 
        /* Map source preference name */
@@ -44,6 +53,8 @@ public class AltosDroidPreferences extends AltosPreferences {
 
                AltosPreferences.init(new AltosDroidPreferencesBackend(context));
 
+               font_size = backend.getInt(fontSizePreference, font_size_medium);
+
                String address = backend.getString(activeDeviceAddressPreference, null);
                String name = backend.getString(activeDeviceNamePreference, null);
 
@@ -107,4 +118,20 @@ public class AltosDroidPreferences extends AltosPreferences {
                        map_source_listeners.remove(l);
                }
        }
+
+       public static int font_size() {
+               synchronized (backend) {
+                       return font_size;
+               }
+       }
+
+       public static void set_font_size(int new_font_size) {
+               synchronized (backend) {
+                       if (font_size != new_font_size) {
+                               font_size = new_font_size;
+                               backend.putInt(fontSizePreference, font_size);
+                               flush_preferences();
+                       }
+               }
+       }
 }