From: Ben Soares Date: Sun, 21 Jun 2020 00:23:37 +0000 (+0100) Subject: JAL-3609 New auto-scale 'formula' for linux HiDPI. Tested to work for UHD screen... X-Git-Tag: Release_2_11_1_1~22^2~17^2~3 X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;h=d53c5e2db2e6a2ed15e15561d417a8f5c60a4669;p=jalview.git JAL-3609 New auto-scale 'formula' for linux HiDPI. Tested to work for UHD screen in various OS display settings. --- diff --git a/getdown/lib/FJVL_VERSION b/getdown/lib/FJVL_VERSION index afcaa01..fdf3dcc 100644 --- a/getdown/lib/FJVL_VERSION +++ b/getdown/lib/FJVL_VERSION @@ -1 +1 @@ -1.8.3-1.2.5_FJVL +1.8.3-1.2.6_FJVL diff --git a/getdown/lib/JVL_VERSION b/getdown/lib/JVL_VERSION index 61aa33c..4492183 100644 --- a/getdown/lib/JVL_VERSION +++ b/getdown/lib/JVL_VERSION @@ -1 +1 @@ -1.8.3-1.2.5_JVL +1.8.3-1.2.6_JVL diff --git a/getdown/lib/getdown-core.jar b/getdown/lib/getdown-core.jar index 8e7c45c..6748a25 100644 Binary files a/getdown/lib/getdown-core.jar and b/getdown/lib/getdown-core.jar differ diff --git a/getdown/lib/getdown-launcher-local.jar b/getdown/lib/getdown-launcher-local.jar index 4f69732..9a27f55 100644 Binary files a/getdown/lib/getdown-launcher-local.jar and b/getdown/lib/getdown-launcher-local.jar differ diff --git a/getdown/lib/getdown-launcher.jar b/getdown/lib/getdown-launcher.jar index 29646f5..e441bc6 100644 Binary files a/getdown/lib/getdown-launcher.jar and b/getdown/lib/getdown-launcher.jar differ diff --git a/getdown/src/getdown/ant/pom.xml b/getdown/src/getdown/ant/pom.xml index 9af441d..65686d2 100644 --- a/getdown/src/getdown/ant/pom.xml +++ b/getdown/src/getdown/ant/pom.xml @@ -4,7 +4,7 @@ com.threerings.getdown getdown - 1.8.3-1.2.5_FJVL + 1.8.3-1.2.6_FJVL getdown-ant diff --git a/getdown/src/getdown/core/pom.xml b/getdown/src/getdown/core/pom.xml index 1563c23..6a9e169 100644 --- a/getdown/src/getdown/core/pom.xml +++ b/getdown/src/getdown/core/pom.xml @@ -4,7 +4,7 @@ com.threerings.getdown getdown - 1.8.3-1.2.5_FJVL + 1.8.3-1.2.6_FJVL getdown-core 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 3ff683e..497900f 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,20 +1,23 @@ package jalview.bin; +import java.awt.HeadlessException; import java.awt.Toolkit; public class HiDPISetting { - private static final int hidpiThreshold = 130; + private static final int hidpiThreshold = 160; - private static final int tallScreenThreshold = 1400; + private static final int hidpiMultiThreshold = 240; - private static final String scalePropertyName = "sun.java2d.uiScale"; + private static final int bigScreenThreshold = 1400; - private static final boolean isAMac; + private static final String scalePropertyName = "sun.java2d.uiScale"; private static final boolean isLinux; - private static final boolean isWindows; + // private static final boolean isAMac; + + // private static final boolean isWindows; public static final String setHiDPIPropertyName = "setHiDPI"; @@ -38,11 +41,19 @@ public class HiDPISetting static { - isAMac = System.getProperty("os.name").indexOf("Mac") > -1; - isLinux = System.getProperty("os.name").toLowerCase() - .indexOf("linux") > -1; - isWindows = System.getProperty("os.name").toLowerCase() - .indexOf("windows") > -1; + String system = System.getProperty("os.name") == null ? null + : System.getProperty("os.name").toLowerCase(); + if (system != null) + { + isLinux = system.indexOf("linux") > -1; + // isAMac = system.indexOf("mac") > -1; + // isWindows = system.indexOf("windows") > -1; + } + else + { + isLinux = false; + // isAMac = isWindows = false; + } } private static void init() @@ -52,6 +63,7 @@ public class HiDPISetting return; } + // get and use command line property values first String setHiDPIProperty = System.getProperty(setHiDPIPropertyName); setHiDPI = setHiDPIProperty != null && setHiDPIProperty.equalsIgnoreCase("true"); @@ -69,14 +81,44 @@ public class HiDPISetting + setHiDPIScaleProperty + ") but not parseable as integer"); } } + if (setHiDPI && setHiDPIScale > 0) + { + setHiDPIScale(setHiDPIScale); + return; + } + + // check to see if the scale property has already been set by something else + // (e.g. the OS) + String existingProperty = System.getProperty(scalePropertyName); + if (existingProperty != null) + { + try + { + int existingPropertyVal = Integer.parseInt(existingProperty); + System.out.println("Existing " + scalePropertyName + " is " + + existingPropertyVal); + if (existingPropertyVal > 1) + { + setHiDPIScale(existingPropertyVal); + return; + } + } catch (NumberFormatException e) + { + System.out.println("Could not convert property " + scalePropertyName + + " vale '" + existingProperty + "' to number"); + } + } + + // Try and auto guess a good scale based on reported DPI (not trustworthy) + // and screen resolution (more trustworthy) - // try and get screen resolution + // get screen dpi try { dpi = Toolkit.getDefaultToolkit().getScreenResolution(); - } catch (Throwable t) + } catch (HeadlessException e) { - System.err.println("Cannot get screen resolution"); + System.err.println("Cannot get screen resolution: " + e.getMessage()); } // try and get screen size height and width @@ -86,48 +128,38 @@ public class HiDPISetting int width = Toolkit.getDefaultToolkit().getScreenSize().width; // using mindimension in case of portrait screens mindimension = Math.min(height, width); - } catch (Throwable t) + } catch (HeadlessException e) { - System.err.println("Cannot get screen size height and width"); + System.err.println( + "Cannot get screen size height and width:" + e.getMessage()); } - if (setHiDPI && setHiDPIScale > 0) - { - scale = setHiDPIScale; - } - else - { - // attempt at a formula for scaling based on screen dpi and mindimension. - // scale - // will be an integer >=1 - if (dpi > 0 && mindimension > 0) - { - scale = Math.min(dpi / hidpiThreshold, - mindimension / tallScreenThreshold) + 1; - } - else if (dpi == 0 && mindimension > tallScreenThreshold) - { - // dpi couldn't be found but the screen has a large vertical pixel count - scale = mindimension / tallScreenThreshold + 1; - } - /* do nothing if mindimension == 0 -- might be just a small HD screen (e.g. Gemini PDA) - else if (mindimension == 0 && dpi > hidpiThreshold) - { - } - */ - } + // attempt at a formula for scaling based on screen dpi and mindimension. + // scale will be an integer >=1. This formula is based on some testing and + // guesswork! + + // scale based on reported dpi. if dpi>hidpiThreshold then scale=2+multiples + // of hidpiMultiThreshold (else scale=1) + // (e.g. dpi of 110 scales 1. dpi of 120 scales 2. dpi of 360 scales 3) + int dpiScale = (dpi - hidpiThreshold > 0) + ? 2 + ((dpi - hidpiThreshold) / hidpiMultiThreshold) + : 1; - // only make a change if scale is changed and other conditions (OS is linux) - // apply, or if setHiDPI has been specified - allowScalePropertyArg = (scale > 1 && isLinux) || setHiDPI; + int dimensionScale = 1 + (mindimension / bigScreenThreshold); - if (allowScalePropertyArg) + // choose larger of dimensionScale or dpiScale (most likely dimensionScale + // as dpiScale often misreported) + int autoScale = Math.max(dpiScale, dimensionScale); + + // only make an automatic change if scale is changed and other conditions + // (OS is linux) apply, or if setHiDPI has been specified + if ((autoScale > 1 && isLinux) || setHiDPI) { - System.out.println("boolean setHiDPI=" + setHiDPI); - System.out.println("DPI detected as " + dpi - + ". Scaling factor set to " + scale + "."); + setHiDPIScale(autoScale); + return; } + // looks like we're not doing any scaling doneInit = true; } diff --git a/getdown/src/getdown/launcher/pom.xml b/getdown/src/getdown/launcher/pom.xml index e8eb824..0410815 100644 --- a/getdown/src/getdown/launcher/pom.xml +++ b/getdown/src/getdown/launcher/pom.xml @@ -4,7 +4,7 @@ com.threerings.getdown getdown - 1.8.3-1.2.5_FJVL + 1.8.3-1.2.6_FJVL getdown-launcher diff --git a/getdown/src/getdown/mvn_cmd b/getdown/src/getdown/mvn_cmd index d10f7a8..25faf6f 100755 --- a/getdown/src/getdown/mvn_cmd +++ b/getdown/src/getdown/mvn_cmd @@ -3,7 +3,7 @@ if [ x$JVLVERSION != x ]; then export VERSION=$JVLVERSION else - export VERSION=1.8.3-1.2.5_JVL + export VERSION=1.8.3-1.2.6_JVL fi if [ x${VERSION%_JVL} = x$VERSION ]; then diff --git a/getdown/src/getdown/pom.xml b/getdown/src/getdown/pom.xml index 1109505..0011325 100644 --- a/getdown/src/getdown/pom.xml +++ b/getdown/src/getdown/pom.xml @@ -10,7 +10,7 @@ com.threerings.getdown getdown pom - 1.8.3-1.2.5_FJVL + 1.8.3-1.2.6_FJVL getdown An application installer and updater. diff --git a/j11lib/getdown-core.jar b/j11lib/getdown-core.jar index 8e7c45c..6748a25 100644 Binary files a/j11lib/getdown-core.jar and b/j11lib/getdown-core.jar differ diff --git a/j8lib/getdown-core.jar b/j8lib/getdown-core.jar index 8e7c45c..6748a25 100644 Binary files a/j8lib/getdown-core.jar and b/j8lib/getdown-core.jar differ diff --git a/src/jalview/bin/HiDPISetting.java b/src/jalview/bin/HiDPISetting.java index 3ff683e..497900f 100644 --- a/src/jalview/bin/HiDPISetting.java +++ b/src/jalview/bin/HiDPISetting.java @@ -1,20 +1,23 @@ package jalview.bin; +import java.awt.HeadlessException; import java.awt.Toolkit; public class HiDPISetting { - private static final int hidpiThreshold = 130; + private static final int hidpiThreshold = 160; - private static final int tallScreenThreshold = 1400; + private static final int hidpiMultiThreshold = 240; - private static final String scalePropertyName = "sun.java2d.uiScale"; + private static final int bigScreenThreshold = 1400; - private static final boolean isAMac; + private static final String scalePropertyName = "sun.java2d.uiScale"; private static final boolean isLinux; - private static final boolean isWindows; + // private static final boolean isAMac; + + // private static final boolean isWindows; public static final String setHiDPIPropertyName = "setHiDPI"; @@ -38,11 +41,19 @@ public class HiDPISetting static { - isAMac = System.getProperty("os.name").indexOf("Mac") > -1; - isLinux = System.getProperty("os.name").toLowerCase() - .indexOf("linux") > -1; - isWindows = System.getProperty("os.name").toLowerCase() - .indexOf("windows") > -1; + String system = System.getProperty("os.name") == null ? null + : System.getProperty("os.name").toLowerCase(); + if (system != null) + { + isLinux = system.indexOf("linux") > -1; + // isAMac = system.indexOf("mac") > -1; + // isWindows = system.indexOf("windows") > -1; + } + else + { + isLinux = false; + // isAMac = isWindows = false; + } } private static void init() @@ -52,6 +63,7 @@ public class HiDPISetting return; } + // get and use command line property values first String setHiDPIProperty = System.getProperty(setHiDPIPropertyName); setHiDPI = setHiDPIProperty != null && setHiDPIProperty.equalsIgnoreCase("true"); @@ -69,14 +81,44 @@ public class HiDPISetting + setHiDPIScaleProperty + ") but not parseable as integer"); } } + if (setHiDPI && setHiDPIScale > 0) + { + setHiDPIScale(setHiDPIScale); + return; + } + + // check to see if the scale property has already been set by something else + // (e.g. the OS) + String existingProperty = System.getProperty(scalePropertyName); + if (existingProperty != null) + { + try + { + int existingPropertyVal = Integer.parseInt(existingProperty); + System.out.println("Existing " + scalePropertyName + " is " + + existingPropertyVal); + if (existingPropertyVal > 1) + { + setHiDPIScale(existingPropertyVal); + return; + } + } catch (NumberFormatException e) + { + System.out.println("Could not convert property " + scalePropertyName + + " vale '" + existingProperty + "' to number"); + } + } + + // Try and auto guess a good scale based on reported DPI (not trustworthy) + // and screen resolution (more trustworthy) - // try and get screen resolution + // get screen dpi try { dpi = Toolkit.getDefaultToolkit().getScreenResolution(); - } catch (Throwable t) + } catch (HeadlessException e) { - System.err.println("Cannot get screen resolution"); + System.err.println("Cannot get screen resolution: " + e.getMessage()); } // try and get screen size height and width @@ -86,48 +128,38 @@ public class HiDPISetting int width = Toolkit.getDefaultToolkit().getScreenSize().width; // using mindimension in case of portrait screens mindimension = Math.min(height, width); - } catch (Throwable t) + } catch (HeadlessException e) { - System.err.println("Cannot get screen size height and width"); + System.err.println( + "Cannot get screen size height and width:" + e.getMessage()); } - if (setHiDPI && setHiDPIScale > 0) - { - scale = setHiDPIScale; - } - else - { - // attempt at a formula for scaling based on screen dpi and mindimension. - // scale - // will be an integer >=1 - if (dpi > 0 && mindimension > 0) - { - scale = Math.min(dpi / hidpiThreshold, - mindimension / tallScreenThreshold) + 1; - } - else if (dpi == 0 && mindimension > tallScreenThreshold) - { - // dpi couldn't be found but the screen has a large vertical pixel count - scale = mindimension / tallScreenThreshold + 1; - } - /* do nothing if mindimension == 0 -- might be just a small HD screen (e.g. Gemini PDA) - else if (mindimension == 0 && dpi > hidpiThreshold) - { - } - */ - } + // attempt at a formula for scaling based on screen dpi and mindimension. + // scale will be an integer >=1. This formula is based on some testing and + // guesswork! + + // scale based on reported dpi. if dpi>hidpiThreshold then scale=2+multiples + // of hidpiMultiThreshold (else scale=1) + // (e.g. dpi of 110 scales 1. dpi of 120 scales 2. dpi of 360 scales 3) + int dpiScale = (dpi - hidpiThreshold > 0) + ? 2 + ((dpi - hidpiThreshold) / hidpiMultiThreshold) + : 1; - // only make a change if scale is changed and other conditions (OS is linux) - // apply, or if setHiDPI has been specified - allowScalePropertyArg = (scale > 1 && isLinux) || setHiDPI; + int dimensionScale = 1 + (mindimension / bigScreenThreshold); - if (allowScalePropertyArg) + // choose larger of dimensionScale or dpiScale (most likely dimensionScale + // as dpiScale often misreported) + int autoScale = Math.max(dpiScale, dimensionScale); + + // only make an automatic change if scale is changed and other conditions + // (OS is linux) apply, or if setHiDPI has been specified + if ((autoScale > 1 && isLinux) || setHiDPI) { - System.out.println("boolean setHiDPI=" + setHiDPI); - System.out.println("DPI detected as " + dpi - + ". Scaling factor set to " + scale + "."); + setHiDPIScale(autoScale); + return; } + // looks like we're not doing any scaling doneInit = true; }