File tree 2 files changed +25
-11
lines changed
2 files changed +25
-11
lines changed Original file line number Diff line number Diff line change @@ -69,7 +69,7 @@ public void actionPerformed(ActionEvent e) {
69
69
Font editorFont = Preferences .getFont ("editor.font" );
70
70
Font font = new Font (consoleFont .getName (), consoleFont .getStyle (), editorFont .getSize ());
71
71
72
- textArea = new TextAreaFIFO (4000000 );
72
+ textArea = new TextAreaFIFO (8000000 );
73
73
textArea .setRows (16 );
74
74
textArea .setColumns (40 );
75
75
textArea .setEditable (false );
@@ -244,11 +244,11 @@ public void actionPerformed(ActionEvent e) {
244
244
final String s = consumeUpdateBuffer ();
245
245
if (s .length () > 0 ) {
246
246
//System.out.println("gui append " + s.length());
247
- boolean scroll = autoscrollBox .isSelected ();
248
- textArea .allowTrim (scroll );
249
- textArea .append (s );
250
- if (scroll ) {
247
+ if (autoscrollBox .isSelected ()) {
248
+ textArea .appendTrim (s );
251
249
textArea .setCaretPosition (textArea .getDocument ().getLength ());
250
+ } else {
251
+ textArea .appendNoTrim (s );
252
252
}
253
253
}
254
254
}
Original file line number Diff line number Diff line change 30
30
31
31
public class TextAreaFIFO extends JTextArea implements DocumentListener {
32
32
private int maxChars ;
33
+ private int trimMaxChars ;
33
34
34
35
private int updateCount ; // limit how often we trim the document
35
36
36
37
private boolean doTrim ;
37
38
38
39
public TextAreaFIFO (int max ) {
39
40
maxChars = max ;
41
+ trimMaxChars = max / 2 ;
40
42
updateCount = 0 ;
41
43
doTrim = true ;
42
44
getDocument ().addDocumentListener (this );
43
45
}
44
46
45
- public void allowTrim (boolean trim ) {
46
- doTrim = trim ;
47
- }
48
-
49
47
public void insertUpdate (DocumentEvent e ) {
50
48
if (++updateCount > 150 && doTrim ) {
51
49
updateCount = 0 ;
@@ -66,13 +64,29 @@ public void changedUpdate(DocumentEvent e) {
66
64
public void trimDocument () {
67
65
int len = 0 ;
68
66
len = getDocument ().getLength ();
69
- if (len > maxChars ) {
70
- int n = len - maxChars ;
67
+ if (len > trimMaxChars ) {
68
+ int n = len - trimMaxChars ;
71
69
//System.out.println("trimDocument: remove " + n + " chars");
72
70
try {
73
71
getDocument ().remove (0 , n );
74
72
} catch (BadLocationException ble ) {
75
73
}
76
74
}
77
75
}
76
+
77
+ public void appendNoTrim (String s ) {
78
+ int free = maxChars - getDocument ().getLength ();
79
+ if (free <= 0 )
80
+ return ;
81
+ if (s .length () > free )
82
+ append (s .substring (0 , free ));
83
+ else
84
+ append (s );
85
+ doTrim = false ;
86
+ }
87
+
88
+ public void appendTrim (String str ) {
89
+ append (str );
90
+ doTrim = true ;
91
+ }
78
92
}
You can’t perform that action at this time.
0 commit comments