From: Ben Soares <b.soares@dundee.ac.uk>
Date: Thu, 22 Apr 2021 14:20:41 +0000 (+0100)
Subject: JAL-3833 Allow setHiDPI and setHiDPIScale to work more usefully in real life
X-Git-Tag: Release_2_11_2_0~47^2~2
X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b7510c12a0fb9028617e25a4b6edb3cc4011142f;p=jalview.git

JAL-3833 Allow setHiDPI and setHiDPIScale to work more usefully in real life
---

diff --git a/src/jalview/bin/HiDPISetting.java b/src/jalview/bin/HiDPISetting.java
index 7a22607..38b7587 100644
--- a/src/jalview/bin/HiDPISetting.java
+++ b/src/jalview/bin/HiDPISetting.java
@@ -68,8 +68,17 @@ public class HiDPISetting
 
     // get and use command line property values first
     String setHiDPIProperty = System.getProperty(setHiDPIPropertyName);
-    setHiDPI = setHiDPIProperty != null
-            && setHiDPIProperty.equalsIgnoreCase("true");
+    boolean setHiDPIPropertyBool = Boolean.parseBoolean(setHiDPIProperty);
+
+    // allow -DsetHiDPI=false to turn off HiDPI scaling
+    if (setHiDPIProperty != null && !setHiDPIPropertyBool)
+    {
+      clear();
+      doneInit = true;
+      return;
+    }
+
+    setHiDPI = setHiDPIProperty != null && setHiDPIPropertyBool;
 
     String setHiDPIScaleProperty = System
             .getProperty(setHiDPIScalePropertyName);
@@ -78,6 +87,12 @@ public class HiDPISetting
       try
       {
         setHiDPIScale = Integer.parseInt(setHiDPIScaleProperty);
+        // if setHiDPIScale property is validly set and setHiDPI property wasn't
+        // attempted to be set we assume setHiDPIScale to be true
+        if (setHiDPIProperty == null)
+        {
+          setHiDPI = true;
+        }
       } catch (NumberFormatException e)
       {
         System.err.println(setHiDPIScalePropertyName + " property give ("