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