| 114 | | FontUIResource default_font = new FontUIResource("AR PL New Sung", Font.PLAIN, 12); |
|---|
| 115 | | Enumeration keys = UIManager.getDefaults().keys(); |
|---|
| 116 | | while (keys.hasMoreElements()) { |
|---|
| 117 | | Object key = keys.nextElement(); |
|---|
| 118 | | Object value = UIManager.get(key); |
|---|
| 119 | | if (value instanceof FontUIResource) { |
|---|
| 120 | | UIManager.put(key, default_font); |
|---|
| | 114 | String new_default_font_str = null; |
|---|
| | 115 | if ( System.getProperty("os.name").equals("Linux") ) { |
|---|
| | 116 | new_default_font_str = "Bitstream Cyberbit"; |
|---|
| | 117 | } else if ( System.getProperty("os.name").startsWith("Windows") ) { |
|---|
| | 118 | new_default_font_str = "Arial Unicode MS"; |
|---|
| | 119 | } |
|---|
| | 120 | |
|---|
| | 121 | if ( new_default_font_str != null ) { |
|---|
| | 122 | |
|---|
| | 123 | FontUIResource default_font = new FontUIResource(new_default_font_str, Font.PLAIN, 12); |
|---|
| | 124 | Enumeration keys = UIManager.getDefaults().keys(); |
|---|
| | 125 | while (keys.hasMoreElements()) { |
|---|
| | 126 | Object key = keys.nextElement(); |
|---|
| | 127 | Object value = UIManager.get(key); |
|---|
| | 128 | if (value instanceof FontUIResource) { |
|---|
| | 129 | UIManager.put(key, default_font); |
|---|
| | 130 | } |
|---|
