--- 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)