diff -r 964b85e04f1f -r de8dbdadda76 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:15:31 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:23:41 2024 +0100
@@ -9,6 +9,8 @@
 
 import javax.swing.JComponent
 
+import scala.collection.mutable
+
 
 object Rich_Text {
   def command(
@@ -21,6 +23,25 @@
     Command.unparsed(source, id = id, results = results, markups = markups)
   }
 
+  def format(
+    msgs: List[XML.Elem],
+    margin: Double,
+    metric: Font_Metric,
+    results: Command.Results
+  ) : List[Command] = {
+    val result = new mutable.ListBuffer[Command]
+    for (msg <- msgs) {
+      if (result.nonEmpty) {
+        result += command(body = Pretty.Separator, id = Document_ID.make())
+      }
+      val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
+      result += command(body = body, id = Markup.Serial.get(msg.markup.properties))
+
+      Exn.Interrupt.expose()
+    }
+    result.toList
+  }
+
   def make_margin(metric: Font_Metric, margin: Int, limit: Int = -1): Int = {
     val m = (margin * metric.average).toInt
     (if (limit < 0) m else m min limit) max 20