()
| 118 | } |
| 119 | |
| 120 | public void applyPreferences() { |
| 121 | |
| 122 | // Update the console text pane font from the preferences. |
| 123 | Font consoleFont = Theme.getFont("console.font"); |
| 124 | Font editorFont = PreferencesData.getFont("editor.font"); |
| 125 | Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize())); |
| 126 | |
| 127 | AttributeSet stdOutStyleOld = stdOutStyle.copyAttributes(); |
| 128 | AttributeSet stdErrStyleOld = stdErrStyle.copyAttributes(); |
| 129 | StyleConstants.setFontSize(stdOutStyle, actualFont.getSize()); |
| 130 | StyleConstants.setFontSize(stdErrStyle, actualFont.getSize()); |
| 131 | |
| 132 | // Re-insert console text with the new preferences if there were changes. |
| 133 | // This assumes that the document has single-child paragraphs (default). |
| 134 | if (!stdOutStyle.isEqual(stdOutStyleOld) || !stdErrStyle.isEqual(stdOutStyleOld)) { |
| 135 | if (out != null) |
| 136 | out.setAttibutes(stdOutStyle); |
| 137 | if (err != null) |
| 138 | err.setAttibutes(stdErrStyle); |
| 139 | |
| 140 | int start; |
| 141 | for (int end = document.getLength() - 1; end >= 0; end = start - 1) { |
| 142 | Element elem = document.getParagraphElement(end); |
| 143 | start = elem.getStartOffset(); |
| 144 | AttributeSet attrs = elem.getElement(0).getAttributes(); |
| 145 | AttributeSet newAttrs; |
| 146 | if (attrs.isEqual(stdErrStyleOld)) { |
| 147 | newAttrs = stdErrStyle; |
| 148 | } else if (attrs.isEqual(stdOutStyleOld)) { |
| 149 | newAttrs = stdOutStyle; |
| 150 | } else { |
| 151 | continue; |
| 152 | } |
| 153 | try { |
| 154 | String text = document.getText(start, end - start); |
| 155 | document.remove(start, end - start); |
| 156 | document.insertString(start, text, newAttrs); |
| 157 | } catch (BadLocationException e) { |
| 158 | // Should only happen when text is async removed (through clear()). |
| 159 | // Accept this case, but throw an error when text could mess up. |
| 160 | if (document.getLength() != 0) { |
| 161 | throw new Error(e); |
| 162 | } |
| 163 | } |
| 164 | } |
| 165 | } |
| 166 | } |
| 167 | |
| 168 | public void clear() { |
| 169 | try { |
nothing calls this directly
no test coverage detected