X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=src%2Fjalview%2Fbin%2FHiDPISetting.java;h=2bce6738ca5f94b59547ed36db1c12bd5972f21c;hb=d654b1f014790b7ae25e6eec631847170a930987;hp=d6d440a363298761080ea333db85f23dc7d60fe3;hpb=baba84a1007310a6da1d81de3abeb2a79563213f;p=jalview.git diff --git a/src/jalview/bin/HiDPISetting.java b/src/jalview/bin/HiDPISetting.java index d6d440a..2bce673 100644 --- a/src/jalview/bin/HiDPISetting.java +++ b/src/jalview/bin/HiDPISetting.java @@ -1,5 +1,27 @@ +/* + * Jalview - A Sequence Alignment Editor and Viewer ($$Version-Rel$$) + * Copyright (C) $$Year-Rel$$ The Jalview Authors + * + * This file is part of Jalview. + * + * Jalview is free software: you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation, either version 3 + * of the License, or (at your option) any later version. + * + * Jalview is distributed in the hope that it will be useful, but + * WITHOUT ANY WARRANTY; without even the implied warranty + * of MERCHANTABILITY or FITNESS FOR A PARTICULAR + * PURPOSE. See the GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Jalview. If not, see . + * The Jalview Authors are detailed in the 'AUTHORS' file. + */ package jalview.bin; +import java.util.Locale; + import java.awt.HeadlessException; public class HiDPISetting @@ -34,6 +56,8 @@ public class HiDPISetting public static int scale = 0; + public final static int MAX_SCALE = 8; + private static boolean doneInit = false; private static boolean allowScalePropertyArg = false; @@ -43,7 +67,7 @@ public class HiDPISetting static { String system = System.getProperty("os.name") == null ? null - : System.getProperty("os.name").toLowerCase(); + : System.getProperty("os.name").toLowerCase(Locale.ROOT); if (system != null) { isLinux = system.indexOf("linux") > -1; @@ -66,8 +90,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); @@ -76,6 +109,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 (" @@ -149,6 +188,16 @@ public class HiDPISetting int dimensionScale = 1 + (mindimension / bigScreenThreshold); + // reject outrageous values -- dpiScale in particular could be mistaken + if (dpiScale > MAX_SCALE) + { + dpiScale = 1; + } + if (dimensionScale > MAX_SCALE) + { + dimensionScale = 1; + } + // choose larger of dimensionScale or dpiScale (most likely dimensionScale // as dpiScale often misreported) int autoScale = Math.max(dpiScale, dimensionScale);