Changeset 10392 in josm

Timestamp:

2016-06-15T20:32:03+02:00 (8 years ago)

Author:

bastiK

Message:

see #9995 - add advanced preference value 'gui.scale'

can be set to test hdpi display or in case the screen resolution is not recognized correctly by the system

File:

• trunk/src/org/openstreetmap/josm/gui/util/GuiSizesHelper.java (modified) (7 diffs)

trunk/src/org/openstreetmap/josm/gui/util/GuiSizesHelper.java

@@ -5 +5 @@
 import java.awt.HeadlessException;
 import java.awt.Toolkit;
+
+import org.openstreetmap.josm.Main;
 
 /**
@@ -20 +22 @@
 
     /** cache value for screen resolution */
-    private static int screenDPI = -1;
+    private static float screenDPI = -1;
 
     /** Request the screen resolution (cached)
      * @return screen resolution in DPI
      */
-    private static int getScreenDPI() {
+    private static float getScreenDPI() {
         if (screenDPI == -1) {
             synchronized (GuiHelper.class) {
                 if (screenDPI == -1) {
-                    try {
-                        screenDPI = Toolkit.getDefaultToolkit().getScreenResolution();
-                    } catch (HeadlessException e) {
-                        screenDPI = 96;
+                    float scalePref = (float) Main.pref.getDouble("gui.scale", 0);
+                    if (scalePref != 0) {
+                        screenDPI = 96f * scalePref;
+                    } else {
+                        try {
+                            screenDPI = Toolkit.getDefaultToolkit().getScreenResolution();
+                        } catch (HeadlessException e) {
+                            screenDPI = 96;
+                        }
                     }
-                        
                 }
             }
@@ -47 +53 @@
      */
     public static float getPixelDensity() {
-        int pixelPerInch = getScreenDPI();
-        return (float) (pixelPerInch / 96.0);
+        float pixelPerInch = getScreenDPI();
+        return pixelPerInch / 96f;
     }
 
@@ -66 +72 @@
     public static int getSizeDpiAdjusted(int size) {
         if (size <= 0) return size;
-        int pixelPerInch = getScreenDPI();
-        return size * pixelPerInch / 96;
+        float pixelPerInch = getScreenDPI();
+        return Math.round(size * pixelPerInch / 96);
     }
 
@@ -77 +83 @@
     public static float getSizeDpiAdjusted(float size) {
         if (size <= 0f) return size;
-        int pixelPerInch = getScreenDPI();
+        float pixelPerInch = getScreenDPI();
         return size * pixelPerInch / 96;
     }
@@ -88 +94 @@
     public static double getSizeDpiAdjusted(double size) {
         if (size <= 0d) return size;
-        int pixelPerInch = getScreenDPI();
+        float pixelPerInch = getScreenDPI();
         return size * pixelPerInch / 96;
     }
@@ -98 +104 @@
      */
     public static Dimension getDimensionDpiAdjusted(Dimension dim) {
-        int pixelPerInch = getScreenDPI();
+        float pixelPerInch = getScreenDPI();
         int width = dim.width, height = dim.height;
         if (dim.width > 0) {
-            width = dim.width * pixelPerInch / 96;
+            width = Math.round(dim.width * pixelPerInch / 96);
         }
 
         if (dim.height > 0) {
-            height = dim.height * pixelPerInch / 96;
+            height = Math.round(dim.height * pixelPerInch / 96);
         }