more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
more Document_Build.running_script, but display it as "Running XYZ";

--- a/src/Pure/PIDE/document_editor.scala	Mon Jan 16 13:48:03 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Mon Jan 16 20:08:15 2023 +0100
@@ -20,27 +20,6 @@
   }
 
 
-  /* progress */
-
-  class Log_Progress(session: Session) extends Progress {
-    def show(text: String): Unit = {}
-
-    private val syslog = session.make_syslog()
-
-    private def update(text: String = syslog.content()): Unit = show(text)
-    private val delay = Delay.first(session.update_delay, gui = true) { update() }
-
-    override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
-
-    def finish(text: String): Unit = GUI_Thread.require {
-      delay.revoke()
-      update(text)
-    }
-
-    GUI_Thread.later { update() }
-  }
-
-
   /* configuration state */
 
   sealed case class State(

--- a/src/Pure/System/progress.scala	Mon Jan 16 13:48:03 2023 +0100
+++ b/src/Pure/System/progress.scala	Mon Jan 16 20:08:15 2023 +0100
@@ -80,3 +80,89 @@
 
   override def toString: String = path.toString
 }
+
+
+/* structured program progress */
+
+object Program_Progress {
+  class Program private[Program_Progress](title: String) {
+    private val output_buffer = new StringBuffer(256)  // synchronized
+
+    def echo(msg: String): Unit = synchronized {
+      if (output_buffer.length() > 0) output_buffer.append('\n')
+      output_buffer.append(msg)
+    }
+
+    val start_time: Time = Time.now()
+    private var stop_time: Option[Time] = None
+    def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) }
+
+    def output(heading: String): (Command.Results, XML.Body) = synchronized {
+      val output_text = output_buffer.toString
+      val elapsed_time = stop_time.map(t => t - start_time)
+
+      val message_prefix = heading + " "
+      val message_suffix =
+        elapsed_time match {
+          case None => " ..."
+          case Some(t) => " ... (" + t.message + " elapsed time)"
+        }
+
+      val (results, message) =
+        if (output_text.isEmpty) {
+          (Command.Results.empty, XML.string(message_prefix + title + message_suffix))
+        }
+        else {
+          val i = Document_ID.make()
+          val results = Command.Results.make(List(i -> Protocol.writeln_message(output_text)))
+          val message =
+            XML.string(message_prefix) :::
+            List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) :::
+            XML.string(message_suffix)
+          (results, message)
+        }
+
+      (results, List(XML.Elem(Markup(Markup.TRACING_MESSAGE, Nil), message)))
+    }
+  }
+}
+
+abstract class Program_Progress extends Progress {
+  private var _finished_programs: List[Program_Progress.Program] = Nil
+  private var _running_program: Option[Program_Progress.Program] = None
+
+  def output(heading: String = "Running"): (Command.Results, XML.Body) = synchronized {
+    val programs = (_running_program.toList ::: _finished_programs).reverse
+    val programs_output = programs.map(_.output(heading))
+    val results = Command.Results.merge(programs_output.map(_._1))
+    val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten
+    (results, body)
+  }
+
+  private def start_program(title: String): Unit = synchronized {
+    _running_program = Some(new Program_Progress.Program(title))
+  }
+
+  def stop_program(): Unit = synchronized {
+    _running_program match {
+      case Some(program) =>
+        program.stop_now()
+        _finished_programs ::= program
+        _running_program = None
+      case None =>
+    }
+  }
+
+  def detect_program(s: String): Option[String]
+
+  override def echo(msg: String): Unit = synchronized {
+    detect_program(msg) match {
+      case Some(title) =>
+        stop_program()
+        start_program(title)
+      case None =>
+        if (_running_program.isEmpty) start_program("program")
+        _running_program.get.echo(msg)
+    }
+  }
+}

--- a/src/Pure/Thy/document_build.scala	Mon Jan 16 13:48:03 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Jan 16 20:08:15 2023 +0100
@@ -132,9 +132,14 @@
     List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
       map(name => texinputs + Path.basic(name))
 
-  def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; "
-  def is_running_script(msg: String): Boolean =
-    msg.startsWith("Running \"") && msg.endsWith("\" ...")
+  def running_script(title: String): String =
+    "echo " + Bash.string("Running program \"" + title + "\" ...") + ";"
+
+  def detect_running_script(s: String): Option[String] =
+    for {
+      s1 <- Library.try_unprefix("Running program \"", s)
+      s2 <- Library.try_unsuffix("\" ...", s1)
+    } yield s2
 
   sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
     def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)

--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Jan 16 13:48:03 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Jan 16 20:08:15 2023 +0100
@@ -35,15 +35,25 @@
     progress: Progress = new Progress,
     process: Future[Unit] = Future.value(()),
     status: Status.Value = Status.FINISHED,
-    output: List[XML.Tree] = Nil
+    output_results: Command.Results = Command.Results.empty,
+    output_main: XML.Body = Nil,
+    output_more: XML.Body = Nil
   ) {
     def run(progress: Progress, process: Future[Unit]): State =
       copy(progress = progress, process = process, status = Status.RUNNING)
 
-    def finish(output: List[XML.Tree]): State =
-      copy(process = Future.value(()), status = Status.FINISHED, output = output)
+    def running(results: Command.Results, body: XML.Body): State =
+      copy(status = Status.RUNNING, output_results = results, output_main = body)
+
+    def finish(output: XML.Body): State =
+      copy(process = Future.value(()), status = Status.FINISHED, output_more = output)
 
-    def ok: Boolean = !output.exists(Protocol.is_error)
+    def output_body: XML.Body =
+      output_main :::
+      (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) :::
+      output_more
+
+    def ok: Boolean = !output_body.exists(Protocol.is_error)
   }
 }
 
@@ -64,7 +74,7 @@
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
-    pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output)
+    pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body)
 
     st.status match {
       case Document_Dockable.Status.WAITING =>
@@ -97,32 +107,34 @@
   })
 
 
-  /* progress log */
+  /* progress */
 
-  private val log_area =
-    new TextArea {
-      editable = false
-      font = GUI.copy_font((new Label).font)
-    }
-  private val scroll_log_area = new ScrollPane(log_area)
+  class Log_Progress extends Program_Progress {
+    progress =>
+
+    override def detect_program(s: String): Option[String] =
+      Document_Build.detect_running_script(s)
 
-  def log_progress(only_running: Boolean = false): Document_Editor.Log_Progress =
-    new Document_Editor.Log_Progress(PIDE.session) {
-      override def show(text: String): Unit =
-        if (text != log_area.text) {
-          log_area.text = text
-          val vertical = scroll_log_area.peer.getVerticalScrollBar
-          vertical.setValue(vertical.getMaximum)
+    private val delay: Delay =
+      Delay.first(PIDE.session.output_delay) {
+        if (!stopped) {
+          running_process(progress)
+          GUI_Thread.later { show_state() }
         }
-      override def echo(msg: String): Unit =
-        if (!only_running || Document_Build.is_running_script(msg)) super.echo(msg)
-    }
+      }
+
+    override def echo(msg: String): Unit = { super.echo(msg); delay.invoke() }
+    override def stop_program(): Unit = { super.stop_program(); delay.invoke() }
+  }
 
 
   /* document build process */
 
   private def init_state(): Unit =
-    current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
+    current_state.change { st =>
+      st.progress.stop()
+      Document_Dockable.State(progress = new Log_Progress)
+    }
 
   private def cancel_process(): Unit =
     current_state.change { st => st.process.cancel(); st }
@@ -130,16 +142,20 @@
   private def await_process(): Unit =
     current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
 
-  private def finish_process(output: List[XML.Tree]): Unit =
+  private def running_process(progress: Log_Progress): Unit = {
+    val (results, body) = progress.output()
+    current_state.change(_.running(results, body))
+  }
+
+  private def finish_process(output: XML.Body): Unit =
     current_state.change(_.finish(output))
 
-  private def run_process(only_running: Boolean = false)(
-    body: Document_Editor.Log_Progress => Unit
-  ): Boolean = {
+  private def run_process(only_running: Boolean = false)(body: Log_Progress => Unit): Boolean = {
     val started =
       current_state.change_result { st =>
         if (st.process.is_finished) {
-          val progress = log_progress(only_running = only_running)
+          st.progress.stop()
+          val progress = new Log_Progress
           val process =
             Future.thread[Unit](name = "Document_Dockable.process") {
               await_process()
@@ -182,7 +198,7 @@
 
   private def document_build(
     session_background: Sessions.Background,
-    progress: Document_Editor.Log_Progress
+    progress: Log_Progress
   ): Unit = {
     val store = JEdit_Sessions.sessions_store(PIDE.options.value)
     val document_selection = PIDE.editor.document_selection()
@@ -197,16 +213,13 @@
           document_session = Some(session_background.base),
           document_selection = document_selection,
           progress = progress)
+
       val variant = session_background.info.documents.head
 
       Isabelle_System.make_directory(Document_Editor.document_output_dir())
       val doc = context.build_document(variant, verbose = true)
 
-      // log
       File.write(Document_Editor.document_output().log, doc.log)
-      GUI_Thread.later { progress.finish(doc.log) }
-
-      // pdf
       Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
       Document_Editor.view_document()
     }
@@ -217,7 +230,7 @@
     PIDE.editor.document_session() match {
       case Some(session_background) if session_background.info.documents.nonEmpty =>
         run_process(only_running = true) { progress =>
-          show_page(log_page)
+          show_page(output_page)
           val result = Exn.capture { document_build(session_background, progress) }
           val msgs =
             result match {
@@ -229,6 +242,8 @@
                 List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
             }
 
+          progress.stop_program()
+          running_process(progress)
           finish_process(Pretty.separate(msgs))
 
           show_state()
@@ -325,12 +340,7 @@
       layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
     }, "Output from build process")
 
-  private val log_page =
-    new TabbedPane.Page("Log", new BorderPanel {
-      layout(scroll_log_area) = BorderPanel.Position.Center
-    }, "Raw log of build process")
-
-  message_pane.pages ++= List(theories_page, log_page, output_page)
+  message_pane.pages ++= List(theories_page, output_page)
 
   set_content(message_pane)