Compute text size relative to key height

Instead of a fixed size that don't work at all for bigger screens.

Other tweaks:
- Use the value-land dimens to vary 'extra_horizontal_margin'
- Move label size to Config, because it can change at runtime (rotation)
- Slightly decrease the size of "long" symbols

1 files changed, 6 insertions, 4 deletions

diff --git a/srcs/juloo.keyboard2/Config.java b/srcs/juloo.keyboard2/Config.java
index ebd7b70..cfd4fb7 100644
--- a/srcs/juloo.keyboard2/Config.java
+++ b/srcs/juloo.keyboard2/Config.java
@@ -15,6 +15,9 @@ final class Config
   public final float marginTop;
   public final float keyPadding;
 
+  public final float labelTextSize;
+  public final float sublabelTextSize;
+
   // From preferences
   public int layout; // Or '-1' for the system defaults
   private float swipe_dist_dp;
@@ -48,6 +51,8 @@ final class Config
     // static values
     marginTop = res.getDimension(R.dimen.margin_top);
     keyPadding = res.getDimension(R.dimen.key_padding);
+    labelTextSize = res.getFloat(R.integer.label_text_size);
+    sublabelTextSize = res.getFloat(R.integer.sublabel_text_size);
     // default values
     layout = -1;
     vibrateEnabled = true;
@@ -85,16 +90,13 @@ final class Config
     // is not the actual size of the keyboard, which will be bigger if the
     // layout has a fifth row. 
     int keyboardHeightPercent;
-    float extra_horizontal_margin;
     if (res.getConfiguration().orientation == Configuration.ORIENTATION_LANDSCAPE) // Landscape mode
     {
       keyboardHeightPercent = 55;
-      extra_horizontal_margin = res.getDimension(R.dimen.landscape_extra_horizontal_margin);
     }
     else
     {
       keyboardHeightPercent = prefs.getInt("keyboard_height", 35);
-      extra_horizontal_margin = 0.f;
     }
     layout = layoutId_of_string(prefs.getString("layout", "system"));
     swipe_dist_dp = Float.valueOf(prefs.getString("swipe_dist", "15"));
@@ -109,7 +111,7 @@ final class Config
     // Do not substract keyVerticalInterval from keyHeight because this is done
     // during rendered.
     keyHeight = dm.heightPixels * keyboardHeightPercent / 100 / 4;
-    horizontalMargin = getDipPref(dm, prefs, "horizontal_margin", horizontalMargin) + extra_horizontal_margin;
+    horizontalMargin = getDipPref(dm, prefs, "horizontal_margin", horizontalMargin) + res.getDimension(R.dimen.extra_horizontal_margin);
     preciseRepeat = prefs.getBoolean("precise_repeat", preciseRepeat);
     characterSize = prefs.getFloat("character_size", characterSize);
     accents = Integer.valueOf(prefs.getString("accents", "1"));