clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
--- a/src/Pure/General/output.scala Mon Nov 11 17:32:40 2019 +0100
+++ b/src/Pure/General/output.scala Tue Nov 12 16:02:29 2019 +0100
@@ -21,25 +21,25 @@
def error_message_text(msg: String): String =
cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
- def writeln(msg: String, stdout: Boolean = false)
+ def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
{
- if (msg != "") {
+ if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(writeln_text(msg) + "\n")
else Console.err.print(writeln_text(msg) + "\n")
}
}
- def warning(msg: String, stdout: Boolean = false)
+ def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
{
- if (msg != "") {
+ if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(warning_text(msg) + "\n")
else Console.err.print(warning_text(msg) + "\n")
}
}
- def error_message(msg: String, stdout: Boolean = false)
+ def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
{
- if (msg != "") {
+ if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(error_message_text(msg) + "\n")
else Console.err.print(error_message_text(msg) + "\n")
}
--- a/src/Pure/System/progress.scala Mon Nov 11 17:32:40 2019 +0100
+++ b/src/Pure/System/progress.scala Tue Nov 12 16:02:29 2019 +0100
@@ -60,7 +60,7 @@
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
{
override def echo(msg: String): Unit =
- Output.writeln(msg, stdout = !stderr)
+ Output.writeln(msg, stdout = !stderr, include_empty = true)
override def theory(theory: Progress.Theory): Unit =
if (verbose) echo(theory.message)