src/Pure/General/output.scala

--- a/src/Pure/General/output.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/output.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -21,7 +21,7 @@
   def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
   def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
 
-  def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+  def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
   {
     if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(writeln_text(msg) + "\n")
@@ -29,7 +29,7 @@
     }
   }
 
-  def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+  def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
   {
     if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(warning_text(msg) + "\n")
@@ -37,7 +37,7 @@
     }
   }
 
-  def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+  def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
   {
     if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(error_message_text(msg) + "\n")