| 186 | } |
| 187 | |
| 188 | public void insertString(String str, SimpleAttributeSet attributes) throws BadLocationException { |
| 189 | // Separate the string into content, newlines and lone carriage |
| 190 | // returns. |
| 191 | // |
| 192 | // Doing so allows lone CRs to move the insertPosition back to the |
| 193 | // start of the line to allow overwriting the most recent line (e.g. |
| 194 | // for a progress bar). Any CR or NL that are immediately followed |
| 195 | // by another NL are bunched together for efficiency, since these |
| 196 | // can just be inserted into the document directly and still be |
| 197 | // correct. |
| 198 | // |
| 199 | // The regex is written so it will necessarily match any string |
| 200 | // completely if applied repeatedly. This is important because any |
| 201 | // part not matched would be silently dropped. |
| 202 | Matcher m = newLinePattern.matcher(str); |
| 203 | |
| 204 | while (m.find()) { |
| 205 | String content = m.group(1); |
| 206 | String newlines = m.group(2); |
| 207 | String crs = m.group(3); |
| 208 | |
| 209 | // Replace (or append if at end of the document) the content first |
| 210 | int replaceLength = Math.min(content.length(), document.getLength() - insertPosition); |
| 211 | document.replace(insertPosition, replaceLength, content, attributes); |
| 212 | insertPosition += content.length(); |
| 213 | |
| 214 | // Then insert any newlines, but always at the end of the document |
| 215 | // e.g. if insertPosition is halfway a line, do not delete |
| 216 | // anything, just add the newline(s) at the end). |
| 217 | if (newlines != null) { |
| 218 | document.insertString(document.getLength(), newlines, attributes); |
| 219 | insertPosition = document.getLength(); |
| 220 | startOfLine = insertPosition; |
| 221 | } |
| 222 | |
| 223 | // Then, for any CRs not followed by newlines, move insertPosition |
| 224 | // to the start of the line. Note that if a newline follows before |
| 225 | // any content in the next call to insertString, it will be added |
| 226 | // at the end of the document anyway, as expected. |
| 227 | if (crs != null) { |
| 228 | insertPosition = startOfLine; |
| 229 | } |
| 230 | } |
| 231 | } |
| 232 | |
| 233 | public String getText() { |
| 234 | return consoleTextPane.getText(); |