- 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;
- dpi = Toolkit.getDefaultToolkit().getScreenResolution();
- scale = dpi / hidpi + 1;
- String forceHiDPISettingProperty = System
- .getProperty(forceHiDPISettingPropertyName);
- forceHiDPISetting = forceHiDPISettingProperty != null
- && forceHiDPISettingProperty.equalsIgnoreCase("true");
- if (doCondition())
+ String system = System.getProperty("os.name") == null ? null
+ : System.getProperty("os.name").toLowerCase(Locale.ROOT);
+ 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()
+ {
+ if (doneInit)
+ {
+ return;
+ }
+
+ // get and use command line property values first
+ String setHiDPIProperty = System.getProperty(setHiDPIPropertyName);
+ 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);
+ if (setHiDPIScaleProperty != null)
+ {
+ 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)
+ {
+ jalview.bin.Console.errPrintln(setHiDPIScalePropertyName
+ + " property give (" + 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);
+ jalview.bin.Console.outPrintln("Existing " + scalePropertyName
+ + " is " + existingPropertyVal);
+ if (existingPropertyVal > 1)
+ {
+ setHiDPIScale(existingPropertyVal);
+ return;
+ }
+ } catch (NumberFormatException e)
+ {
+ jalview.bin.Console.outPrintln(
+ "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)
+
+ // get screen dpi
+ screenInfo = getScreenInfo();
+ try