-1.8.3-1.2.5_FJVL
+1.8.3-1.2.6_FJVL
-1.8.3-1.2.5_JVL
+1.8.3-1.2.6_JVL
<parent>
<groupId>com.threerings.getdown</groupId>
<artifactId>getdown</artifactId>
- <version>1.8.3-1.2.5_FJVL</version>
+ <version>1.8.3-1.2.6_FJVL</version>
</parent>
<artifactId>getdown-ant</artifactId>
<parent>
<groupId>com.threerings.getdown</groupId>
<artifactId>getdown</artifactId>
- <version>1.8.3-1.2.5_FJVL</version>
+ <version>1.8.3-1.2.6_FJVL</version>
</parent>
<artifactId>getdown-core</artifactId>
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";
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()
return;
}
+ // get and use command line property values first
String setHiDPIProperty = System.getProperty(setHiDPIPropertyName);
setHiDPI = setHiDPIProperty != null
&& setHiDPIProperty.equalsIgnoreCase("true");
+ 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
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;
}
<parent>
<groupId>com.threerings.getdown</groupId>
<artifactId>getdown</artifactId>
- <version>1.8.3-1.2.5_FJVL</version>
+ <version>1.8.3-1.2.6_FJVL</version>
</parent>
<artifactId>getdown-launcher</artifactId>
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
<groupId>com.threerings.getdown</groupId>
<artifactId>getdown</artifactId>
<packaging>pom</packaging>
- <version>1.8.3-1.2.5_FJVL</version>
+ <version>1.8.3-1.2.6_FJVL</version>
<name>getdown</name>
<description>An application installer and updater.</description>
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";
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()
return;
}
+ // get and use command line property values first
String setHiDPIProperty = System.getProperty(setHiDPIPropertyName);
setHiDPI = setHiDPIProperty != null
&& setHiDPIProperty.equalsIgnoreCase("true");
+ 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
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;
}
git://source.jalview.org / jalview.git / commitdiff