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