JAL-3609 changed property names to something more palatable and catered for portrait...

diff --git a/getdown/lib/getdown-core.jar b/getdown/lib/getdown-core.jar
index 37ba110..927b3a5 100644 (file)
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 86b1251..27c6758 100644 (file)
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 0df8d7c..10d8c10 100644 (file)
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 (file)
--- 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 37ba110..927b3a5 100644 (file)
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 37ba110..927b3a5 100644 (file)
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 (file)
--- 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;