diff -r 206dd586f3d7 -r 964b85e04f1f src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import javax.swing.JComponent
+
+
 object Rich_Text {
   def command(
     body: XML.Body = Nil,
@@ -17,4 +20,12 @@
     val markups = Command.Markups.init(Markup_Tree.from_XML(body))
     Command.unparsed(source, id = id, results = results, markups = markups)
   }
+
+  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
+  }
+
+  def component_margin(metric: Font_Metric, component: JComponent): Int =
+    make_margin(metric, (component.getWidth.toDouble / metric.average_width).toInt)
 }