(Editor editor)
| 59 | Color outlineColor; |
| 60 | |
| 61 | public ModeSelector(Editor editor) { |
| 62 | title = editor.getMode().getTitle(); //.toUpperCase(); |
| 63 | |
| 64 | addMouseListener(new MouseAdapter() { |
| 65 | public void mousePressed(MouseEvent event) { |
| 66 | JPopupMenu popup = editor.getModePopup(); |
| 67 | popup.show(ModeSelector.this, event.getX(), event.getY()); |
| 68 | } |
| 69 | }); |
| 70 | |
| 71 | updateTheme(); |
| 72 | } |
| 73 | |
| 74 | public void updateTheme() { |
| 75 | titleFont = Theme.getFont("mode.title.font"); |
nothing calls this directly
no test coverage detected