From: Ben Soares 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;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 ("