From 8025245946be1f451bf2e49704c2527be4135a97 Mon Sep 17 00:00:00 2001
From: "Silas S. Brown" <ssb22@cam.ac.uk>
Date: Tue, 3 Sep 2019 08:48:06 +0100
Subject: [PATCH] Update Annotator Generator
---
annogen.py | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/annogen.py b/annogen.py
index bae021d..2ae1cc9 100644
--- a/annogen.py
+++ b/annogen.py
@@ -1,6 +1,6 @@
#!/usr/bin/env python2
-program_name = "Annotator Generator v0.68 (c) 2012-19 Silas S. Brown"
+program_name = "Annotator Generator v0.681 (c) 2012-19 Silas S. Brown"
# See http://people.ds.cam.ac.uk/ssb22/adjuster/annogen.html
@@ -1778,6 +1778,7 @@ android_src += r"""
browser.setWebChromeClient(new WebChromeClient());"""
if android_template: android_src += r"""
float fs = getResources().getConfiguration().fontScale; // from device accessibility settings
+ if (fs < 1.0f) fs = 1.0f; // bug in at least some versions of Android 8 returns 0 for fontScale
final float fontScale=fs*fs; // for backward compatibility with older annogen (and pre-Android 4 version that still sets setDefaultFontSize) : unconfirmed reports say the OS scales the size units anyway, so we've been squaring fontScale all along, which is probably just as well because old Android versions don't offer much range in their settings"""
android_src += r"""
@TargetApi(1)
@@ -2136,7 +2137,9 @@ if android_template: android_src += r"""
}"""
else: android_src += r"""
if(Integer.valueOf(Build.VERSION.SDK) >= 3) browser.getSettings().setBuiltInZoomControls(true);
- final int size=Math.round(16*getResources().getConfiguration().fontScale); // from device accessibility settings (might be squared if OS does it too, but that's OK because the settings don't give enough of a range)
+ float fs = getResources().getConfiguration().fontScale; // from device accessibility settings
+ if (fs < 1.0f) fs = 1.0f; // bug in at least some versions of Android 8 returns 0 for fontScale
+ final int size=Math.round(16*fs); // from device accessibility settings (might be squared if OS does it too, but that's OK because the settings don't give enough of a range)
browser.getSettings().setDefaultFontSize(size);
browser.getSettings().setDefaultFixedFontSize(size);"""
android_src += r"""
--
GitLab