package jalview.bin;
+import java.util.Locale;
+
import java.awt.HeadlessException;
public class HiDPISetting
public static int scale = 0;
+ public final static int MAX_SCALE = 8;
+
private static boolean doneInit = false;
private static boolean allowScalePropertyArg = false;
static
{
String system = System.getProperty("os.name") == null ? null
- : System.getProperty("os.name").toLowerCase();
+ : System.getProperty("os.name").toLowerCase(Locale.ROOT);
if (system != null)
{
isLinux = system.indexOf("linux") > -1;
// get and use command line property values first
String setHiDPIProperty = System.getProperty(setHiDPIPropertyName);
- setHiDPI = setHiDPIProperty != null
- && setHiDPIProperty.equalsIgnoreCase("true");
+ boolean setHiDPIPropertyBool = Boolean.parseBoolean(setHiDPIProperty);
+
+ // allow -DsetHiDPI=false to turn off HiDPI scaling
+ if (setHiDPIProperty != null && !setHiDPIPropertyBool)
+ {
+ clear();
+ doneInit = true;
+ return;
+ }
+
+ setHiDPI = setHiDPIProperty != null && setHiDPIPropertyBool;
String setHiDPIScaleProperty = System
.getProperty(setHiDPIScalePropertyName);
try
{
setHiDPIScale = Integer.parseInt(setHiDPIScaleProperty);
+ // if setHiDPIScale property is validly set and setHiDPI property wasn't
+ // attempted to be set we assume setHiDPIScale to be true
+ if (setHiDPIProperty == null)
+ {
+ setHiDPI = true;
+ }
} catch (NumberFormatException e)
{
System.err.println(setHiDPIScalePropertyName + " property give ("
int dimensionScale = 1 + (mindimension / bigScreenThreshold);
+ // reject outrageous values -- dpiScale in particular could be mistaken
+ if (dpiScale > MAX_SCALE) {
+ dpiScale = 1;
+ }
+ if (dimensionScale > MAX_SCALE) {
+ dimensionScale = 1;
+ }
+
// choose larger of dimensionScale or dpiScale (most likely dimensionScale
// as dpiScale often misreported)
int autoScale = Math.max(dpiScale, dimensionScale);
return allowScalePropertyArg ? getScalePropertyArg(scale) : null;
}
+ public static void setScaleProperty(int s)
+ {
+ System.setProperty(scalePropertyName, String.valueOf(s));
+ }
+
+ public static void setScaleProperty()
+ {
+ init();
+ if (allowScalePropertyArg)
+ {
+ setScaleProperty(scale);
+ }
+ }
+
public static void clear()
{
setHiDPI = false;