File tree Expand file tree Collapse file tree 2 files changed +25
-3
lines changed
app/src/processing/app/ui Expand file tree Collapse file tree 2 files changed +25
-3
lines changed Original file line number Diff line number Diff line change @@ -2293,8 +2293,22 @@ public void prepareRun() {
2293
2293
internalCloseRunner ();
2294
2294
statusEmpty ();
2295
2295
2296
- // do this to advance/clear the terminal window / dos prompt / etc
2297
- for (int i = 0 ; i < 10 ; i ++) System .out .println ();
2296
+ int headPadding ;
2297
+
2298
+ try {
2299
+ headPadding = Preferences .getInteger ("console.head_padding" );
2300
+ } catch (NullPointerException e ) {
2301
+ // We need to handle this exception to take care of old versions of
2302
+ // preference files, i.e., "defaults.txt" and "preferences.txt" which
2303
+ // may not have the attribute 'console.head_padding'.
2304
+ headPadding = 10 ;
2305
+ }
2306
+
2307
+ // Do this to advance/clear the terminal window / dos prompt / etc.
2308
+ // This may be useful especially when 'console.auto_clear' is false.
2309
+ // TODO: use `console.message()` instead of `System.out.println()`?
2310
+ // i.e. for (int i = 0; i < headPadding; i++) console.message("\n", false);
2311
+ for (int i = 0 ; i < headPadding ; i ++) System .out .println ();
2298
2312
2299
2313
// clear the console on each run, unless the user doesn't want to
2300
2314
if (Preferences .getBoolean ("console.auto_clear" )) {
Original file line number Diff line number Diff line change @@ -165,8 +165,16 @@ console.font.size = 12
165
165
# number of lines to show by default
166
166
console.lines = 4
167
167
168
- # set to false to disable automatically clearing the console
168
+ # Number of blank lines to advance/clear console.
169
+ # Note that those lines are also printed in the terminal when
170
+ # Processing is executed there.
171
+ # Setting to 0 stops this behavior.
172
+ console.head_padding = 10
173
+
174
+ # Set to false to disable automatically clearing the console
169
175
# each time 'run' is hit
176
+ # If one sets it to false, one may also want to set 'console.head_padding'
177
+ # to a positive number to separate outputs from different runs.
170
178
console.auto_clear = true
171
179
172
180
# number of days of history to keep around before cleaning
You can’t perform that action at this time.
0 commit comments