From bfa6a392c8abfa3311672401ac6a85aea514d16c Mon Sep 17 00:00:00 2001 From: Junology Date: Fri, 17 Jan 2025 17:21:39 +0900 Subject: [PATCH 1/3] add 'console.head_padding' option --- app/src/processing/app/ui/Editor.java | 18 ++++++++++++++++-- build/shared/lib/defaults.txt | 10 +++++++++- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index 3babbb6dfb..a063141205 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -2293,8 +2293,22 @@ public void prepareRun() { 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 f6265357cd..6e3e00f0d6 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 From f1e4085671ef6a0b6edf159998c4e7b2c9508fd2 Mon Sep 17 00:00:00 2001 From: Junology Date: Fri, 17 Jan 2025 19:04:00 +0900 Subject: [PATCH 2/3] make blank lines padding only in the IDE console and not in terminal --- app/src/processing/app/ui/Editor.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index a063141205..fc22b87a1a 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -2306,9 +2306,7 @@ public void prepareRun() { // 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(); + for (int i = 0; i < headPadding; i++) console.message("\n", false); // clear the console on each run, unless the user doesn't want to if (Preferences.getBoolean("console.auto_clear")) { From a25a0fb6b35591370544dc0a99cfe4a3b243822a Mon Sep 17 00:00:00 2001 From: Junology Date: Fri, 17 Jan 2025 21:16:53 +0900 Subject: [PATCH 3/3] skip unnecessary error handling in reading 'console.head_padding' --- app/src/processing/app/ui/Editor.java | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index fc22b87a1a..3b33119cf7 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -2293,19 +2293,9 @@ public void prepareRun() { internalCloseRunner(); statusEmpty(); - 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. + int headPadding = Preferences.getInteger("console.head_padding"); for (int i = 0; i < headPadding; i++) console.message("\n", false); // clear the console on each run, unless the user doesn't want to