mirror of
https://github.com/processing/processing4.git
synced 2026-01-24 00:41:07 +01:00
add 'console.head_padding' option
This commit is contained in:
@@ -2293,8 +2293,22 @@ public abstract class Editor extends JFrame implements RunnerListener {
|
||||
internalCloseRunner();
|
||||
statusEmpty();
|
||||
|
||||
// do this to advance/clear the terminal window / dos prompt / etc
|
||||
for (int i = 0; i < 10; i++) System.out.println();
|
||||
int headPadding;
|
||||
|
||||
try {
|
||||
headPadding = Preferences.getInteger("console.head_padding");
|
||||
} catch (NullPointerException e) {
|
||||
// We need to handle this exception to take care of old versions of
|
||||
// preference files, i.e., "defaults.txt" and "preferences.txt" which
|
||||
// may not have the attribute 'console.head_padding'.
|
||||
headPadding = 10;
|
||||
}
|
||||
|
||||
// Do this to advance/clear the terminal window / dos prompt / etc.
|
||||
// This may be useful especially when 'console.auto_clear' is false.
|
||||
// TODO: use `console.message()` instead of `System.out.println()`?
|
||||
// i.e. for (int i = 0; i < headPadding; i++) console.message("\n", false);
|
||||
for (int i = 0; i < headPadding; i++) System.out.println();
|
||||
|
||||
// clear the console on each run, unless the user doesn't want to
|
||||
if (Preferences.getBoolean("console.auto_clear")) {
|
||||
|
||||
@@ -165,8 +165,16 @@ console.font.size = 12
|
||||
# number of lines to show by default
|
||||
console.lines = 4
|
||||
|
||||
# set to false to disable automatically clearing the console
|
||||
# Number of blank lines to advance/clear console.
|
||||
# Note that those lines are also printed in the terminal when
|
||||
# Processing is executed there.
|
||||
# Setting to 0 stops this behavior.
|
||||
console.head_padding = 10
|
||||
|
||||
# Set to false to disable automatically clearing the console
|
||||
# each time 'run' is hit
|
||||
# If one sets it to false, one may also want to set 'console.head_padding'
|
||||
# to a positive number to separate outputs from different runs.
|
||||
console.auto_clear = true
|
||||
|
||||
# number of days of history to keep around before cleaning
|
||||
|
||||
Reference in New Issue
Block a user