From b7510c12a0fb9028617e25a4b6edb3cc4011142f Mon Sep 17 00:00:00 2001 From: Ben Soares Date: Thu, 22 Apr 2021 15:20:41 +0100 Subject: [PATCH] JAL-3833 Allow setHiDPI and setHiDPIScale to work more usefully in real life --- src/jalview/bin/HiDPISetting.java | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) 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 (" -- 1.7.10.2