(Base base)
| 65 | private SimpleAttributeSet stdErrStyle; |
| 66 | |
| 67 | public EditorConsole(Base base) { |
| 68 | document = new DefaultStyledDocument(); |
| 69 | |
| 70 | consoleTextPane = new JTextPane(document); |
| 71 | consoleTextPane.setEditable(false); |
| 72 | DefaultCaret caret = (DefaultCaret) consoleTextPane.getCaret(); |
| 73 | caret.setUpdatePolicy(DefaultCaret.NEVER_UPDATE); |
| 74 | consoleTextPane.setFocusTraversalKeysEnabled(false); |
| 75 | |
| 76 | Color backgroundColour = Theme.getColor("console.color"); |
| 77 | consoleTextPane.setBackground(backgroundColour); |
| 78 | |
| 79 | Font consoleFont = Theme.getFont("console.font"); |
| 80 | Font editorFont = PreferencesData.getFont("editor.font"); |
| 81 | Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize())); |
| 82 | |
| 83 | stdOutStyle = new SimpleAttributeSet(); |
| 84 | StyleConstants.setForeground(stdOutStyle, Theme.getColor("console.output.color")); |
| 85 | StyleConstants.setBackground(stdOutStyle, backgroundColour); |
| 86 | StyleConstants.setFontSize(stdOutStyle, actualFont.getSize()); |
| 87 | StyleConstants.setFontFamily(stdOutStyle, actualFont.getFamily()); |
| 88 | StyleConstants.setBold(stdOutStyle, actualFont.isBold()); |
| 89 | StyleConstants.setItalic(stdOutStyle, actualFont.isItalic()); |
| 90 | |
| 91 | consoleTextPane.setParagraphAttributes(stdOutStyle, true); |
| 92 | |
| 93 | stdErrStyle = new SimpleAttributeSet(); |
| 94 | StyleConstants.setForeground(stdErrStyle, Theme.getColor("console.error.color")); |
| 95 | StyleConstants.setBackground(stdErrStyle, backgroundColour); |
| 96 | StyleConstants.setFontSize(stdErrStyle, actualFont.getSize()); |
| 97 | StyleConstants.setFontFamily(stdErrStyle, actualFont.getFamily()); |
| 98 | StyleConstants.setBold(stdErrStyle, actualFont.isBold()); |
| 99 | StyleConstants.setItalic(stdErrStyle, actualFont.isItalic()); |
| 100 | |
| 101 | JPanel noWrapPanel = new JPanel(new BorderLayout()); |
| 102 | noWrapPanel.add(consoleTextPane); |
| 103 | |
| 104 | setViewportView(noWrapPanel); |
| 105 | getVerticalScrollBar().setUnitIncrement(7); |
| 106 | |
| 107 | // calculate height of a line of text in pixels |
| 108 | // and size window accordingly |
| 109 | FontMetrics metrics = getFontMetrics(actualFont); |
| 110 | int height = metrics.getAscent() + metrics.getDescent(); |
| 111 | int lines = PreferencesData.getInteger("console.lines"); |
| 112 | setPreferredSize(new Dimension(100, (height * lines))); |
| 113 | setMinimumSize(new Dimension(100, (height * lines))); |
| 114 | |
| 115 | // Add font size adjustment listeners. |
| 116 | if (base != null) |
| 117 | base.addEditorFontResizeListeners(consoleTextPane); |
| 118 | } |
| 119 | |
| 120 | public void applyPreferences() { |
| 121 |
nothing calls this directly
no test coverage detected