diff -r 056657540039 -r 41374ed08c9f src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 14:58:05 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 15:10:51 2024 +0100
@@ -41,7 +41,7 @@
   ) : List[Formatted] = {
     val result = new mutable.ListBuffer[Formatted]
     for (msg <- msgs) {
-      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator, Command.Results.empty)
+      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator, results)
 
       val id = Protocol_Message.get_serial(msg)
       val body = Pretty.formatted(List(msg), margin = margin, metric = metric)