| 915 | // A 5-minute search didn't turn up any such event in the Java API. |
| 916 | // Also, should we use the Toolkit associated with the editor window? |
| 917 | static private boolean checkRetina() { |
| 918 | if (Platform.isMacOS()) { |
| 919 | GraphicsEnvironment env = GraphicsEnvironment.getLocalGraphicsEnvironment(); |
| 920 | GraphicsDevice device = env.getDefaultScreenDevice(); |
| 921 | |
| 922 | try { |
| 923 | Field field = device.getClass().getDeclaredField("scale"); |
| 924 | if (field != null) { |
| 925 | field.setAccessible(true); |
| 926 | Object scale = field.get(device); |
| 927 | |
| 928 | if (scale instanceof Integer && ((Integer)scale).intValue() == 2) { |
| 929 | return true; |
| 930 | } |
| 931 | } |
| 932 | } catch (Exception ignore) { } |
| 933 | } |
| 934 | return false; |
| 935 | } |
| 936 | |
| 937 | |
| 938 | // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |