tuned output: less empty lines;

isabelle-prover · May 27, 2024 · 7b0c610 · 7b0c610
1 parent c6ad324
commit 7b0c610
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/linter_base/src/linter.scala b/linter_base/src/linter.scala
@@ -165,8 +165,10 @@ object Linter {
           case Some(snapshot) =>
             val report = Linter.lint_snapshot(snapshot, selection)
 
-            if (console)
-              progress.echo(presenter.to_string(presenter.present(report, header = true)))
+            if (console) {
+              val msg = presenter.to_string(presenter.present(report, header = true))
+              progress.echo_if(msg.nonEmpty, msg)
+            }
 
             Some(report)
         }

diff --git a/linter_base/src/presenter.scala b/linter_base/src/presenter.scala
@@ -99,9 +99,10 @@ case class Text_Presenter(do_underline: Boolean) extends Presenter[String] {
     Utils.map_accum_l(source.trim.split("\n").toList, range, underline).mkString("\n").trim
   }
 
-  override def to_string(report: String): String = if (report.isEmpty) "" else report
+  override def to_string(report: String): String = if (report.isBlank) "" else report
 
-  override def mk_string(reports: List[String]): String = reports.filterNot(_.isBlank).mkString("\n")
+  override def mk_string(reports: List[String]): String =
+    reports.filterNot(_.isBlank).mkString("\n")
 
   override def present(
     lint_report: Linter.Report,