# HG changeset patch
# User wenzelm
# Date 1760358267 -7200
# Node ID bcc69ca4ac10b75cd7d2e6b8513a7716d007c072
# Parent  2f75f2495e3eff72c4764b9edd216f63769bbcfb
clarified signature: more robust and uniform out.flush (following b11587195c70);

diff -r 2f75f2495e3e -r bcc69ca4ac10 src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Sun Oct 12 15:11:29 2025 +0200
+++ b/src/Pure/General/output.scala	Mon Oct 13 14:24:27 2025 +0200
@@ -6,8 +6,6 @@
 
 package isabelle
 
-import java.io.PrintStream
-
 
 object Output {
   def writeln_text(msg: String): String = Protocol_Message.clean_output(msg)
@@ -19,11 +17,14 @@
   def error_message_text(msg: String): String =
     error_message_prefix(Protocol_Message.clean_output(msg))
 
-  def stream(stdout: Boolean = false): PrintStream =
-    if (stdout) Console.out else Console.err
+  def print_stream(s: String, stdout: Boolean = false): Unit = {
+    val out = if (stdout) Console.out else Console.err
+    out.print(s)
+    out.flush()
+  }
 
   def output(s: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
-    if (s.nonEmpty || include_empty) stream(stdout = stdout).print(s + "\n")
+    if (s.nonEmpty || include_empty) print_stream(s + "\n", stdout = stdout)
 
   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
     output(writeln_text(msg), stdout = stdout, include_empty = include_empty)
@@ -34,11 +35,6 @@
   def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
     output(error_message_text(msg), stdout = stdout, include_empty = include_empty)
 
-  def delete_lines(lines: Int, stdout: Boolean = false): Unit = {
-    if (lines > 0) {
-      val out = stream(stdout = stdout)
-      out.print("\u001b[" + lines + "F\u001b[J")
-      out.flush()
-    }
-  }
+  def delete_lines(lines: Int, stdout: Boolean = false): Unit =
+    if (lines > 0) print_stream("\u001b[" + lines + "F\u001b[J", stdout = stdout)
 }