X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=getdown%2Fsrc%2Fgetdown%2Fcore%2Fsrc%2Fmain%2Fjava%2Fjalview%2Fbin%2FHiDPISetting.java;h=871a6f7539022e3b5598041c8029f731a285e719;hb=e83ce5d8ef826fc0b509a51f154abdf734501077;hp=75106ccb4d04ea987fe0aa7196db47508d2a2b67;hpb=d74ee697c7ac0a0ffca7854f787821a726839e4b;p=jalview.git diff --git a/getdown/src/getdown/core/src/main/java/jalview/bin/HiDPISetting.java b/getdown/src/getdown/core/src/main/java/jalview/bin/HiDPISetting.java index 75106cc..871a6f7 100644 --- a/getdown/src/getdown/core/src/main/java/jalview/bin/HiDPISetting.java +++ b/getdown/src/getdown/core/src/main/java/jalview/bin/HiDPISetting.java @@ -1,8 +1,29 @@ +/* + * 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.awt.HeadlessException; import java.util.Locale; +import jalview.util.ErrorLog; public class HiDPISetting { @@ -36,6 +57,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; @@ -68,8 +91,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,9 +110,15 @@ 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 (" + ErrorLog.errPrintln(setHiDPIScalePropertyName + " property give (" + setHiDPIScaleProperty + ") but not parseable as integer"); } } @@ -98,7 +136,7 @@ public class HiDPISetting try { int existingPropertyVal = Integer.parseInt(existingProperty); - System.out.println("Existing " + scalePropertyName + " is " + ErrorLog.outPrintln("Existing " + scalePropertyName + " is " + existingPropertyVal); if (existingPropertyVal > 1) { @@ -107,8 +145,9 @@ public class HiDPISetting } } catch (NumberFormatException e) { - System.out.println("Could not convert property " + scalePropertyName - + " vale '" + existingProperty + "' to number"); + ErrorLog.outPrintln( + "Could not convert property " + scalePropertyName + + " vale '" + existingProperty + "' to number"); } } @@ -122,7 +161,11 @@ public class HiDPISetting dpi = screenInfo.getScreenResolution(); } catch (HeadlessException e) { - System.err.println("Cannot get screen resolution: " + e.getMessage()); + if (isLinux) + { + ErrorLog.errPrintln( + "Cannot get screen resolution: " + e.getMessage()); + } } // try and get screen size height and width @@ -134,8 +177,11 @@ public class HiDPISetting mindimension = Math.min(height, width); } catch (HeadlessException e) { - System.err.println( - "Cannot get screen size height and width:" + e.getMessage()); + if (isLinux) + { + ErrorLog.errPrintln("Cannot get screen size height and width:" + + e.getMessage()); + } } // attempt at a formula for scaling based on screen dpi and mindimension. @@ -151,6 +197,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);