X-Git-Url: https://git.gag.com/?a=blobdiff_plain;f=altosdroid%2Fapp%2Fsrc%2Fmain%2Fjava%2Forg%2Faltusmetrum%2FAltosDroid%2FAltosDroidPreferences.java;h=f23955685389d43ed93bf4e12adf626676a375e2;hb=6e3c4493cfa8d92d96808d14d1c12abb35ecb442;hp=6ec9e4d19b867802c38af3b257989f2b55441b73;hpb=d7ef39ba104a1ac6024af875c730a645f282719f;p=fw%2Faltos

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 6ec9e4d1..f2395568 100644
--- 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();
+			}
+		}
+	}
 }