+ // 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;
+ }