diff -r 3585a1a77ad1 -r 85fc3b482924 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Tue Nov 12 11:16:36 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Tue Nov 12 11:32:07 2024 +0100
@@ -26,26 +26,21 @@
 
   /* format */
 
-  sealed case class Formatted(id: Document_ID.Generic, body: XML.Body, results: Command.Results) {
+  sealed case class Formatted(id: Document_ID.Generic, body: XML.Body) {
     lazy val text: String = XML.content(body)
-    lazy val command: Command =
-      Command.unparsed(text, id = id, results = results,
-        markups = Command.Markups.init(Markup_Tree.from_XML(body)))
+    lazy val markups: Command.Markups = Command.Markups.init(Markup_Tree.from_XML(body))
+    def command(results: Command.Results): Command =
+      Command.unparsed(text, id = id, results = results, markups = markups)
   }
 
-  def format(
-    msgs: List[XML.Elem],
-    margin: Double,
-    metric: Font_Metric,
-    results: Command.Results = Command.Results.empty
-  ) : List[Formatted] = {
+  def format(msgs: List[XML.Elem], margin: Double, metric: Font_Metric): List[Formatted] = {
     val result = new mutable.ListBuffer[Formatted]
     for (msg <- msgs) {
-      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator, results)
+      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator)
 
       val id = Protocol_Message.get_serial(msg)
       val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
-      result += Formatted(id, body, results)
+      result += Formatted(id, body)
 
       Exn.Interrupt.expose()
     }