# HG changeset patch
# User wenzelm
# Date 1731238400 -3600
# Node ID d25a241502c1b2724ce01cab33fc61118843612a
# Parent  b242c7603e0864668b0269cfdbda180f3f62ac80
tuned comments;

diff -r b242c7603e08 -r d25a241502c1 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:29:32 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:33:20 2024 +0100
@@ -13,6 +13,19 @@
 
 
 object Rich_Text {
+  /* margin */
+
+  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)
+
+
+  /* format */
+
   def command(
     body: XML.Body = Nil,
     id: Document_ID.Command = Document_ID.none,
@@ -41,12 +54,4 @@
     }
     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
-  }
-
-  def component_margin(metric: Font_Metric, component: JComponent): Int =
-    make_margin(metric, (component.getWidth.toDouble / metric.average_width).toInt)
 }