From: Ben Soares Date: Tue, 19 May 2020 19:32:27 +0000 (+0100) Subject: JAL-3609 changed property names to something more palatable and catered for portrait... X-Git-Tag: Develop-2_11_2_0-d20201215~15^2~44 X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;h=62d10e940e86310c996659dd729aa61f7fd516fd;p=jalview.git JAL-3609 changed property names to something more palatable and catered for portrait screens --- diff --git a/getdown/lib/getdown-core.jar b/getdown/lib/getdown-core.jar index 8cc0fba..764dbc6 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 9b00b2d..50d9d57 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 13fa5f8..7f3df08 100644 Binary files a/getdown/lib/getdown-launcher.jar and b/getdown/lib/getdown-launcher.jar differ 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 770fb27..4472a19 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 @@ -16,17 +16,19 @@ public class HiDPISetting private static final boolean isWindows; - public static final String forceHiDPISettingPropertyName = "forceHiDPISetting"; + public static final String setHiDPIPropertyName = "setHiDPI"; - public static final String forceHiDPISettingScalePropertyName = "forceHiDPISettingScale"; + public static final String setHiDPIScalePropertyName = "setHiDPIScale"; - private static final boolean forceHiDPISetting; + private static boolean setHiDPI = false; - private static final int forceHiDPISettingScale; + private static int setHiDPIScale = 0; public static int dpi = 0; - public static int height = 0; + public static int maxdimension = 0; + + public static int width = 0; public static int scale = 0; @@ -41,37 +43,32 @@ public class HiDPISetting .indexOf("linux") > -1; isWindows = System.getProperty("os.name").toLowerCase() .indexOf("windows") > -1; + } - String forceHiDPISettingProperty = System - .getProperty(forceHiDPISettingPropertyName); - forceHiDPISetting = forceHiDPISettingProperty != null - && forceHiDPISettingProperty.equalsIgnoreCase("true"); + private static void init() + { + if (doneInit) + { + return; + } - int tryForceHiDPISettingScale = 0; - String forceHiDPISettingScaleProperty = System - .getProperty(forceHiDPISettingScalePropertyName); - if (forceHiDPISettingScaleProperty != null) + String setHiDPIProperty = System.getProperty(setHiDPIPropertyName); + setHiDPI = setHiDPIProperty != null + && setHiDPIProperty.equalsIgnoreCase("true"); + + String setHiDPIScaleProperty = System + .getProperty(setHiDPIScalePropertyName); + if (setHiDPIScaleProperty != null) { try { - tryForceHiDPISettingScale = Integer - .parseInt(forceHiDPISettingScaleProperty); + setHiDPIScale = Integer.parseInt(setHiDPIScaleProperty); } catch (NumberFormatException e) { - System.err.println(forceHiDPISettingScalePropertyName - + " property give (" + forceHiDPISettingScaleProperty - + ") but not parseable as integer"); + System.err.println(setHiDPIScalePropertyName + " property give (" + + setHiDPIScaleProperty + ") but not parseable as integer"); } } - forceHiDPISettingScale = tryForceHiDPISettingScale; - } - - private void init() - { - if (doneInit) - { - return; - } // try and get screen resolution try @@ -82,32 +79,51 @@ public class HiDPISetting System.err.println("Cannot get screen resolution"); } - // try and get screen size height + // try and get screen size height and width try { - height = Toolkit.getDefaultToolkit().getScreenSize().height; + int height = Toolkit.getDefaultToolkit().getScreenSize().height; + int width = Toolkit.getDefaultToolkit().getScreenSize().width; + // using maxdimension in case of portrait screens + maxdimension = Math.max(height, width); } catch (Throwable t) { - System.err.println("Cannot get screen size height"); + System.err.println("Cannot get screen size height and width"); } - if (forceHiDPISetting && forceHiDPISettingScale > 0) + if (setHiDPI && setHiDPIScale > 0) { - scale = forceHiDPISettingScale; + scale = setHiDPIScale; } else { - // attempt at a formula for scaling based on screen dpi and height. scale + // attempt at a formula for scaling based on screen dpi and maxdimension. + // scale // will be an integer >=1 - scale = Math.min(dpi / hidpiThreshold, height / tallScreenThreshold) - + 1; + if (dpi > 0 && maxdimension > 0) + { + scale = Math.min(dpi / hidpiThreshold, + maxdimension / tallScreenThreshold) + 1; + } + else if (dpi == 0 && maxdimension > tallScreenThreshold) + { + // dpi couldn't be found but the screen has a large vertical pixel count + scale = maxdimension / tallScreenThreshold + 1; + } + /* do nothing if maxdimension == 0 -- might be just a small HD screen (e.g. Gemini PDA) + else if (maxdimension == 0 && dpi > hidpiThreshold) + { + } + */ } - allowScalePropertyArg = (scale > 1 && isLinux) || forceHiDPISetting; + // 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; if (allowScalePropertyArg) { - System.out.println("boolean forceHiDPISetting=" + forceHiDPISetting); + System.out.println("boolean setHiDPI=" + setHiDPI); System.out.println("DPI detected as " + dpi + ". Scaling factor set to " + scale + "."); } @@ -115,8 +131,16 @@ public class HiDPISetting doneInit = true; } - public static synchronized String getScalePropertyArg() + public static void setHiDPIScale(int s) + { + scale = s; + allowScalePropertyArg = true; + doneInit = true; + } + + public static String getScalePropertyArg() { + init(); // HiDPI setting. Just looking at Linux to start with. Test with Windows. return allowScalePropertyArg ? "-D" + scalePropertyName + "=" + scale : null; diff --git a/j11lib/getdown-core.jar b/j11lib/getdown-core.jar index 8cc0fba..764dbc6 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 8cc0fba..764dbc6 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 770fb27..4472a19 100644 --- a/src/jalview/bin/HiDPISetting.java +++ b/src/jalview/bin/HiDPISetting.java @@ -16,17 +16,19 @@ public class HiDPISetting private static final boolean isWindows; - public static final String forceHiDPISettingPropertyName = "forceHiDPISetting"; + public static final String setHiDPIPropertyName = "setHiDPI"; - public static final String forceHiDPISettingScalePropertyName = "forceHiDPISettingScale"; + public static final String setHiDPIScalePropertyName = "setHiDPIScale"; - private static final boolean forceHiDPISetting; + private static boolean setHiDPI = false; - private static final int forceHiDPISettingScale; + private static int setHiDPIScale = 0; public static int dpi = 0; - public static int height = 0; + public static int maxdimension = 0; + + public static int width = 0; public static int scale = 0; @@ -41,37 +43,32 @@ public class HiDPISetting .indexOf("linux") > -1; isWindows = System.getProperty("os.name").toLowerCase() .indexOf("windows") > -1; + } - String forceHiDPISettingProperty = System - .getProperty(forceHiDPISettingPropertyName); - forceHiDPISetting = forceHiDPISettingProperty != null - && forceHiDPISettingProperty.equalsIgnoreCase("true"); + private static void init() + { + if (doneInit) + { + return; + } - int tryForceHiDPISettingScale = 0; - String forceHiDPISettingScaleProperty = System - .getProperty(forceHiDPISettingScalePropertyName); - if (forceHiDPISettingScaleProperty != null) + String setHiDPIProperty = System.getProperty(setHiDPIPropertyName); + setHiDPI = setHiDPIProperty != null + && setHiDPIProperty.equalsIgnoreCase("true"); + + String setHiDPIScaleProperty = System + .getProperty(setHiDPIScalePropertyName); + if (setHiDPIScaleProperty != null) { try { - tryForceHiDPISettingScale = Integer - .parseInt(forceHiDPISettingScaleProperty); + setHiDPIScale = Integer.parseInt(setHiDPIScaleProperty); } catch (NumberFormatException e) { - System.err.println(forceHiDPISettingScalePropertyName - + " property give (" + forceHiDPISettingScaleProperty - + ") but not parseable as integer"); + System.err.println(setHiDPIScalePropertyName + " property give (" + + setHiDPIScaleProperty + ") but not parseable as integer"); } } - forceHiDPISettingScale = tryForceHiDPISettingScale; - } - - private void init() - { - if (doneInit) - { - return; - } // try and get screen resolution try @@ -82,32 +79,51 @@ public class HiDPISetting System.err.println("Cannot get screen resolution"); } - // try and get screen size height + // try and get screen size height and width try { - height = Toolkit.getDefaultToolkit().getScreenSize().height; + int height = Toolkit.getDefaultToolkit().getScreenSize().height; + int width = Toolkit.getDefaultToolkit().getScreenSize().width; + // using maxdimension in case of portrait screens + maxdimension = Math.max(height, width); } catch (Throwable t) { - System.err.println("Cannot get screen size height"); + System.err.println("Cannot get screen size height and width"); } - if (forceHiDPISetting && forceHiDPISettingScale > 0) + if (setHiDPI && setHiDPIScale > 0) { - scale = forceHiDPISettingScale; + scale = setHiDPIScale; } else { - // attempt at a formula for scaling based on screen dpi and height. scale + // attempt at a formula for scaling based on screen dpi and maxdimension. + // scale // will be an integer >=1 - scale = Math.min(dpi / hidpiThreshold, height / tallScreenThreshold) - + 1; + if (dpi > 0 && maxdimension > 0) + { + scale = Math.min(dpi / hidpiThreshold, + maxdimension / tallScreenThreshold) + 1; + } + else if (dpi == 0 && maxdimension > tallScreenThreshold) + { + // dpi couldn't be found but the screen has a large vertical pixel count + scale = maxdimension / tallScreenThreshold + 1; + } + /* do nothing if maxdimension == 0 -- might be just a small HD screen (e.g. Gemini PDA) + else if (maxdimension == 0 && dpi > hidpiThreshold) + { + } + */ } - allowScalePropertyArg = (scale > 1 && isLinux) || forceHiDPISetting; + // 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; if (allowScalePropertyArg) { - System.out.println("boolean forceHiDPISetting=" + forceHiDPISetting); + System.out.println("boolean setHiDPI=" + setHiDPI); System.out.println("DPI detected as " + dpi + ". Scaling factor set to " + scale + "."); } @@ -115,8 +131,16 @@ public class HiDPISetting doneInit = true; } - public static synchronized String getScalePropertyArg() + public static void setHiDPIScale(int s) + { + scale = s; + allowScalePropertyArg = true; + doneInit = true; + } + + public static String getScalePropertyArg() { + init(); // HiDPI setting. Just looking at Linux to start with. Test with Windows. return allowScalePropertyArg ? "-D" + scalePropertyName + "=" + scale : null;