- void remove_frequency_menu() {
- if (frequencies != null) {
- menu_bar.remove(frequencies);
- menu_bar.repaint();
- frequencies = null;
- }
+ void disable_frequency_menu() {
+ if (frequency_listener == null)
+ return;
+ frequencies.removeActionListener(frequency_listener);
+ menu_bar.remove(frequencies);
+ menu_bar.repaint();
+ frequency_listener = null;