# HG changeset patch
# User wenzelm
# Date 1730992438 -3600
# Node ID 92aa6f7b470cfc808407d0b5b1c8412ae46cd957
# Parent  365b9aac4363c129aa692226b3cdb5a6f0efd5ee
clarified output representation: postpone Pretty.separate;

diff -r 365b9aac4363 -r 92aa6f7b470c src/Pure/System/program_progress.scala
--- a/src/Pure/System/program_progress.scala	Thu Nov 07 16:03:53 2024 +0100
+++ b/src/Pure/System/program_progress.scala	Thu Nov 07 16:13:58 2024 +0100
@@ -20,7 +20,7 @@
     private var stop_time: Option[Time] = None
     def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) }
 
-    def output(): (Command.Results, XML.Body) = synchronized {
+    def output(): (Command.Results, XML.Elem) = synchronized {
       val output_text = output_buffer.toString
       val elapsed_time = stop_time.map(t => t - start_time)
 
@@ -45,7 +45,7 @@
           (results, message)
         }
 
-      (results, List(XML.elem(Markup.TRACING_MESSAGE, message)))
+      (results, XML.elem(Markup.TRACING_MESSAGE, message))
     }
   }
 }
@@ -58,12 +58,11 @@
   private var _finished_programs: List[Program_Progress.Program] = Nil
   private var _running_program: Option[Program_Progress.Program] = None
 
-  def output(): (Command.Results, XML.Body) = synchronized {
+  def output(): (Command.Results, List[XML.Elem]) = synchronized {
     val programs = (_running_program.toList ::: _finished_programs).reverse
     val programs_output = programs.map(_.output())
     val results = Command.Results.merge(programs_output.map(_._1))
-    val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten
-    (results, body)
+    (results, programs_output.map(_._2))
   }
 
   private def start_program(heading: String, title: String): Unit = synchronized {
diff -r 365b9aac4363 -r 92aa6f7b470c src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 07 16:03:53 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 07 16:13:58 2024 +0100
@@ -30,24 +30,21 @@
     process: Future[Unit] = Future.value(()),
     progress: Progress = new Progress,
     output_results: Command.Results = Command.Results.empty,
-    output_main: XML.Body = Nil,
-    output_more: XML.Body = Nil
+    output_main: List[XML.Elem] = Nil,
+    output_more: List[XML.Elem] = Nil
   ) {
     def running: Boolean = !process.is_finished
 
     def run(process: Future[Unit], progress: Progress, reset_pending: Boolean): State =
       copy(process = process, progress = progress, pending = if (reset_pending) false else pending)
 
-    def output(results: Command.Results, body: XML.Body): State =
-      copy(output_results = results, output_main = body, output_more = Nil)
+    def output(results: Command.Results, main: List[XML.Elem]): State =
+      copy(output_results = results, output_main = main, output_more = Nil)
 
-    def finish(body: XML.Body): State =
-      copy(process = Future.value(()), output_more = body)
+    def finish(more: List[XML.Elem]): State =
+      copy(process = Future.value(()), output_more = more)
 
-    def output_body: XML.Body =
-      output_main :::
-      (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) :::
-      output_more
+    def output_all: List[XML.Elem] = output_main ::: output_more
 
     def reset(): State = {
       process.cancel()
@@ -74,7 +71,8 @@
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
-    pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body)
+    pretty_text_area.update(Document.Snapshot.init, st.output_results,
+      Pretty.separate(st.output_all))
 
     if (st.running) process_indicator.update("Running document build process ...", 15)
     else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5)
@@ -138,8 +136,8 @@
     current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
 
   private def output_process(progress: Log_Progress): Unit = {
-    val (results, body) = progress.output()
-    current_state.change(_.output(results, body))
+    val (results, main) = progress.output()
+    current_state.change(_.output(results, main))
   }
 
   private def pending_process(): Unit =
@@ -152,7 +150,7 @@
       }
     }
 
-  private def finish_process(output: XML.Body): Unit =
+  private def finish_process(output: List[XML.Elem]): Unit =
     current_state.change { st =>
       if (st.pending) {
         delay_auto_build.revoke()
@@ -230,7 +228,7 @@
         progress.stop_program()
         output_process(progress)
         progress.stop()
-        finish_process(Pretty.separate(msgs))
+        finish_process(msgs)
 
         show_page(output_page)
       }