diff -r 206dd586f3d7 -r 964b85e04f1f src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -25,10 +25,16 @@
 
 class Font_Metric(
   val font: Font = Font_Metric.default_font,
-  val context: FontRenderContext = Font_Metric.default_context,
-  standard_margin: Double => Int = _ => Pretty.default_margin.toInt) extends Pretty.Metric
+  val context: FontRenderContext = Font_Metric.default_context) extends Pretty.Metric
 {
   override def toString: String = font.toString
+  override def hashCode: Int = font.hashCode
+
+  override def equals(that: Any): Boolean =
+    that match {
+      case other: Font_Metric => font == other.font && context == other.context
+      case _ => false
+    }
 
   def string_bounds(str: String): Rectangle2D = font.getStringBounds(str, context)
   def string_width(str: String): Double = string_bounds(str).getWidth
@@ -48,19 +54,4 @@
     string_width(s1) / unit
   }
   def average: Double = average_width / unit
-
-  def make_margin(margin: Int, limit: Int = -1): Int = {
-    val m = (margin * average).toInt
-    (if (limit < 0) m else m min limit) max 20
-  }
-  val margin: Int = make_margin(standard_margin(average_width))
-
-  override lazy val hashCode: Int = (font, context, margin).hashCode
-
-  override def equals(that: Any): Boolean =
-    that match {
-      case other: Font_Metric =>
-        font == other.font && context == other.context && margin == other.margin
-      case _ => false
-    }
 }