| 1159 | // A 5-minute search didn't turn up any such event in the Java API. |
| 1160 | // Also, should we use the Toolkit associated with the editor window? |
| 1161 | static private boolean checkRetina() { |
| 1162 | AffineTransform tx = GraphicsEnvironment |
| 1163 | .getLocalGraphicsEnvironment() |
| 1164 | .getDefaultScreenDevice() |
| 1165 | .getDefaultConfiguration() |
| 1166 | .getDefaultTransform(); |
| 1167 | |
| 1168 | return Math.round(tx.getScaleX()) == 2; |
| 1169 | } |
| 1170 | |
| 1171 | |
| 1172 | // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |