mirror of
https://github.com/arduino/Arduino.git
synced 2025-03-13 10:29:35 +01:00
parent
c4f5cafd33
commit
b70a7d088e
@ -25,8 +25,11 @@ package processing.app.linux;
|
||||
import processing.app.PreferencesData;
|
||||
import processing.app.legacy.PConstants;
|
||||
|
||||
import java.awt.Font;
|
||||
import java.io.File;
|
||||
|
||||
import javax.swing.UIManager;
|
||||
|
||||
|
||||
/**
|
||||
* Used by Base for platform-specific tweaking, for instance finding the
|
||||
@ -117,4 +120,19 @@ public class Platform extends processing.app.Platform {
|
||||
public String getName() {
|
||||
return PConstants.platformNames[PConstants.LINUX];
|
||||
}
|
||||
|
||||
private int detectedDpi = -1;
|
||||
|
||||
@Override
|
||||
public int getSystemDPI() {
|
||||
if (detectedDpi != -1)
|
||||
return detectedDpi;
|
||||
|
||||
// we observed that JMenu fonts in java follows the
|
||||
// System DPI settings, so we compare it to the standard
|
||||
// font size (12) to obtain a rough estimate of DPI.
|
||||
Font menuFont = UIManager.getFont("Menu.font");
|
||||
detectedDpi = menuFont.getSize() * 96 / 12;
|
||||
return detectedDpi;
|
||||
}
|
||||
}
|
||||
|
Loading…
x
Reference in New Issue
Block a user