diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index 3babbb6df..a06314120 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -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")) { diff --git a/build/shared/lib/defaults.txt b/build/shared/lib/defaults.txt index f6265357c..6e3e00f0d 100644 --- a/build/shared/lib/defaults.txt +++ b/build/shared/lib/defaults.txt @@ -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