# HG changeset patch
# User wenzelm
# Date 1731166454 -3600
# Node ID 4794576828df2624dfac18b69dece4c4836a9300
# Parent  84cf218e052a912f1b920729d5f6bbd1d6d2d986
clarified signature: include standard margin in object equality;

diff -r 84cf218e052a -r 4794576828df src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Sat Nov 09 16:01:07 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Sat Nov 09 16:34:14 2024 +0100
@@ -25,16 +25,10 @@
 
 class Font_Metric(
   val font: Font = Font_Metric.default_font,
-  val context: FontRenderContext = Font_Metric.default_context) extends Pretty.Metric
+  val context: FontRenderContext = Font_Metric.default_context,
+  standard_margin: Double => Int = _ => Pretty.default_margin.toInt) 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
@@ -55,8 +49,18 @@
   }
   def average: Double = average_width / unit
 
-  def pretty_margin(margin: Int, limit: Int = -1): Int = {
+  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
+    }
 }
diff -r 84cf218e052a -r 4794576828df src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 09 16:01:07 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 09 16:34:14 2024 +0100
@@ -233,7 +233,10 @@
   /* graphics range */
 
   def font_metric(painter: TextAreaPainter): Font_Metric =
-    new Font_Metric(font = painter.getFont, context = painter.getFontRenderContext)
+    new Font_Metric(
+      font = painter.getFont,
+      context = painter.getFontRenderContext,
+      standard_margin = (average_width: Double) => (painter.getWidth.toDouble / average_width).toInt)
 
   case class Gfx_Range(x: Int, y: Int, length: Int)
 
diff -r 84cf218e052a -r 4794576828df src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:01:07 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:34:14 2024 +0100
@@ -88,8 +88,6 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.font_metric(getPainter)
-      val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.average_width).toInt)
-
       val output = current_output
       val snapshot = current_base_snapshot
       val results = current_base_results
@@ -97,7 +95,8 @@
       future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
-          val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
+          val formatted =
+            Pretty.formatted(Pretty.separate(output), margin = metric.margin, metric = metric)
           val rich_text = Command.rich_text(body = formatted, results = results)
           val rendering =
             try { JEdit_Rendering(snapshot, rich_text) }
diff -r 84cf218e052a -r 4794576828df src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Nov 09 16:01:07 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Nov 09 16:34:14 2024 +0100
@@ -248,7 +248,7 @@
       val geometry = JEdit_Lib.window_geometry(pretty_tooltip, painter)
       val metric = JEdit_Lib.font_metric(painter)
       val margin =
-        metric.pretty_margin(rendering.tooltip_margin,
+        metric.make_margin(rendering.tooltip_margin,
           limit = ((w_max - geometry.deco_width) / metric.average_width).toInt)
 
       val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)