Read and apply new values from the preferences, either because the app is just starting up, or the user just finished messing with things in the Preferences window.
()
| 489 | * with things in the Preferences window. |
| 490 | */ |
| 491 | public void applyPreferences() { |
| 492 | boolean external = PreferencesData.getBoolean("editor.external"); |
| 493 | saveMenuItem.setEnabled(!external); |
| 494 | saveAsMenuItem.setEnabled(!external); |
| 495 | for (EditorTab tab: tabs) { |
| 496 | tab.applyPreferences(); |
| 497 | } |
| 498 | console.applyPreferences(); |
| 499 | if (serialMonitor != null) { |
| 500 | serialMonitor.applyPreferences(); |
| 501 | } |
| 502 | } |
| 503 | |
| 504 | |
| 505 | // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
no test coverage detected