JAL-3609 system properties to force a scale, or automatically choose based on OS...

diff --git a/getdown/lib/getdown-core.jar b/getdown/lib/getdown-core.jar
index 8e3ade4..37ba110 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 b826dbf..86b1251 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 e311ace..0df8d7c 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 bea9dae..770fb27 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
@@ -4,11 +4,9 @@ import java.awt.Toolkit;
 
 public class HiDPISetting
 {
-  public static final int dpi;
+  private static final int hidpiThreshold = 130;
 
-  public static final int scale;
-
-  private static final int hidpi = 110;
+  private static final int tallScreenThreshold = 1300;
 
   private static final String scalePropertyName = "sun.java2d.uiScale";
 
@@ -20,8 +18,22 @@ public class HiDPISetting
 
   public static final String forceHiDPISettingPropertyName = "forceHiDPISetting";
 
+  public static final String forceHiDPISettingScalePropertyName = "forceHiDPISettingScale";
+
   private static final boolean forceHiDPISetting;
 
+  private static final int forceHiDPISettingScale;
+
+  public static int dpi = 0;
+
+  public static int height = 0;
+
+  public static int scale = 0;
+
+  private static boolean doneInit = false;
+
+  private static boolean allowScalePropertyArg = false;
+
   static
   {
     isAMac = System.getProperty("os.name").indexOf("Mac") > -1;
@@ -29,34 +41,84 @@ public class HiDPISetting
             .indexOf("linux") > -1;
     isWindows = System.getProperty("os.name").toLowerCase()
             .indexOf("windows") > -1;
-    dpi = Toolkit.getDefaultToolkit().getScreenResolution();
-    scale = dpi / hidpi + 1;
+
     String forceHiDPISettingProperty = System
             .getProperty(forceHiDPISettingPropertyName);
     forceHiDPISetting = forceHiDPISettingProperty != null
             && forceHiDPISettingProperty.equalsIgnoreCase("true");
-    if (doCondition())
+
+    int tryForceHiDPISettingScale = 0;
+    String forceHiDPISettingScaleProperty = System
+            .getProperty(forceHiDPISettingScalePropertyName);
+    if (forceHiDPISettingScaleProperty != null)
+    {
+      try
+      {
+        tryForceHiDPISettingScale = Integer
+                .parseInt(forceHiDPISettingScaleProperty);
+      } catch (NumberFormatException e)
+      {
+        System.err.println(forceHiDPISettingScalePropertyName
+                + " property give (" + forceHiDPISettingScaleProperty
+                + ") but not parseable as integer");
+      }
+    }
+    forceHiDPISettingScale = tryForceHiDPISettingScale;
+  }
+
+  private void init()
+  {
+    if (doneInit)
+    {
+      return;
+    }
+
+    // try and get screen resolution
+    try
+    {
+      dpi = Toolkit.getDefaultToolkit().getScreenResolution();
+    } catch (Throwable t)
+    {
+      System.err.println("Cannot get screen resolution");
+    }
+
+    // try and get screen size height
+    try
+    {
+      height = Toolkit.getDefaultToolkit().getScreenSize().height;
+    } catch (Throwable t)
+    {
+      System.err.println("Cannot get screen size height");
+    }
+
+    if (forceHiDPISetting && forceHiDPISettingScale > 0)
+    {
+      scale = forceHiDPISettingScale;
+    }
+    else
+    {
+      // attempt at a formula for scaling based on screen dpi and height. scale
+      // will be an integer >=1
+      scale = Math.min(dpi / hidpiThreshold, height / tallScreenThreshold)
+              + 1;
+    }
+
+    allowScalePropertyArg = (scale > 1 && isLinux) || forceHiDPISetting;
+
+    if (allowScalePropertyArg)
     {
-      System.out.println("Property '" + forceHiDPISettingPropertyName + "'="
-              + forceHiDPISettingProperty);
       System.out.println("boolean forceHiDPISetting=" + forceHiDPISetting);
       System.out.println("DPI detected as " + dpi
               + ". Scaling factor set to " + scale + ".");
     }
-  }
 
-  private static synchronized boolean doCondition()
-  {
-    return (scale > 1 && isLinux) || forceHiDPISetting;
+    doneInit = true;
   }
 
   public static synchronized String getScalePropertyArg()
   {
     // HiDPI setting. Just looking at Linux to start with. Test with Windows.
-    if (doCondition())
-    {
-      return "-D" + scalePropertyName + "=" + scale;
-    }
-    return null;
+    return allowScalePropertyArg ? "-D" + scalePropertyName + "=" + scale
+            : null;
   }
 }

diff --git a/j11lib/getdown-core.jar b/j11lib/getdown-core.jar
index 8e3ade4..37ba110 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 8e3ade4..37ba110 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 bea9dae..770fb27 100644 (file)
--- a/src/jalview/bin/HiDPISetting.java
+++ b/src/jalview/bin/HiDPISetting.java
@@ -4,11 +4,9 @@ import java.awt.Toolkit;
 
 public class HiDPISetting
 {
-  public static final int dpi;
+  private static final int hidpiThreshold = 130;
 
-  public static final int scale;
-
-  private static final int hidpi = 110;
+  private static final int tallScreenThreshold = 1300;
 
   private static final String scalePropertyName = "sun.java2d.uiScale";
 
@@ -20,8 +18,22 @@ public class HiDPISetting
 
   public static final String forceHiDPISettingPropertyName = "forceHiDPISetting";
 
+  public static final String forceHiDPISettingScalePropertyName = "forceHiDPISettingScale";
+
   private static final boolean forceHiDPISetting;
 
+  private static final int forceHiDPISettingScale;
+
+  public static int dpi = 0;
+
+  public static int height = 0;
+
+  public static int scale = 0;
+
+  private static boolean doneInit = false;
+
+  private static boolean allowScalePropertyArg = false;
+
   static
   {
     isAMac = System.getProperty("os.name").indexOf("Mac") > -1;
@@ -29,34 +41,84 @@ public class HiDPISetting
             .indexOf("linux") > -1;
     isWindows = System.getProperty("os.name").toLowerCase()
             .indexOf("windows") > -1;
-    dpi = Toolkit.getDefaultToolkit().getScreenResolution();
-    scale = dpi / hidpi + 1;
+
     String forceHiDPISettingProperty = System
             .getProperty(forceHiDPISettingPropertyName);
     forceHiDPISetting = forceHiDPISettingProperty != null
             && forceHiDPISettingProperty.equalsIgnoreCase("true");
-    if (doCondition())
+
+    int tryForceHiDPISettingScale = 0;
+    String forceHiDPISettingScaleProperty = System
+            .getProperty(forceHiDPISettingScalePropertyName);
+    if (forceHiDPISettingScaleProperty != null)
+    {
+      try
+      {
+        tryForceHiDPISettingScale = Integer
+                .parseInt(forceHiDPISettingScaleProperty);
+      } catch (NumberFormatException e)
+      {
+        System.err.println(forceHiDPISettingScalePropertyName
+                + " property give (" + forceHiDPISettingScaleProperty
+                + ") but not parseable as integer");
+      }
+    }
+    forceHiDPISettingScale = tryForceHiDPISettingScale;
+  }
+
+  private void init()
+  {
+    if (doneInit)
+    {
+      return;
+    }
+
+    // try and get screen resolution
+    try
+    {
+      dpi = Toolkit.getDefaultToolkit().getScreenResolution();
+    } catch (Throwable t)
+    {
+      System.err.println("Cannot get screen resolution");
+    }
+
+    // try and get screen size height
+    try
+    {
+      height = Toolkit.getDefaultToolkit().getScreenSize().height;
+    } catch (Throwable t)
+    {
+      System.err.println("Cannot get screen size height");
+    }
+
+    if (forceHiDPISetting && forceHiDPISettingScale > 0)
+    {
+      scale = forceHiDPISettingScale;
+    }
+    else
+    {
+      // attempt at a formula for scaling based on screen dpi and height. scale
+      // will be an integer >=1
+      scale = Math.min(dpi / hidpiThreshold, height / tallScreenThreshold)
+              + 1;
+    }
+
+    allowScalePropertyArg = (scale > 1 && isLinux) || forceHiDPISetting;
+
+    if (allowScalePropertyArg)
     {
-      System.out.println("Property '" + forceHiDPISettingPropertyName + "'="
-              + forceHiDPISettingProperty);
       System.out.println("boolean forceHiDPISetting=" + forceHiDPISetting);
       System.out.println("DPI detected as " + dpi
               + ". Scaling factor set to " + scale + ".");
     }
-  }
 
-  private static synchronized boolean doCondition()
-  {
-    return (scale > 1 && isLinux) || forceHiDPISetting;
+    doneInit = true;
   }
 
   public static synchronized String getScalePropertyArg()
   {
     // HiDPI setting. Just looking at Linux to start with. Test with Windows.
-    if (doCondition())
-    {
-      return "-D" + scalePropertyName + "=" + scale;
-    }
-    return null;
+    return allowScalePropertyArg ? "-D" + scalePropertyName + "=" + scale
+            : null;
   }
 }