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