From d63162b5a10abd8c3cc9b7c47cc4fb7c2bb2a4dd Mon Sep 17 00:00:00 2001 From: Cristian Maglie Date: Thu, 3 Nov 2016 16:29:41 +0200 Subject: [PATCH] Added Platform.getSystemDPI() API --- app/src/processing/app/Theme.java | 2 +- arduino-core/src/processing/app/Platform.java | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/app/src/processing/app/Theme.java b/app/src/processing/app/Theme.java index cea6e6fe4..bfa393498 100644 --- a/app/src/processing/app/Theme.java +++ b/app/src/processing/app/Theme.java @@ -122,7 +122,7 @@ public class Theme { return scale; } catch (NumberFormatException ignore) { } - return 100; + return BaseNoGui.getPlatform().getSystemDPI() * 100 / 96; } static public int scale(int size) { diff --git a/arduino-core/src/processing/app/Platform.java b/arduino-core/src/processing/app/Platform.java index f829699bd..0f3d59175 100644 --- a/arduino-core/src/processing/app/Platform.java +++ b/arduino-core/src/processing/app/Platform.java @@ -333,4 +333,9 @@ public class Platform { public void fixSettingsLocation() throws Exception { //noop } + + public int getSystemDPI() { + return 96; + } + }