# HG changeset patch
# User wenzelm
# Date 1731073469 -3600
# Node ID 4e3d461afa105b02d79af4a8c4d7cbb0b0c4f9c7
# Parent  874e12fb6c3d9a55b380cd5b0ecae5c6ab557db9
clarified signature: more uniform;

diff -r 874e12fb6c3d -r 4e3d461afa10 src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Fri Nov 08 13:55:54 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Fri Nov 08 14:44:29 2024 +0100
@@ -54,4 +54,9 @@
     string_width(s1) / unit
   }
   def average: Double = average_width / unit
+
+  def pretty_margin(margin: Int, limit: Double = Double.NaN): Double = {
+    val m = margin * average
+    (if (limit.isNaN) m else m min limit) max 20.0
+  }
 }
diff -r 874e12fb6c3d -r 4e3d461afa10 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 13:55:54 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 14:44:29 2024 +0100
@@ -88,7 +88,7 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.font_metric(getPainter)
-      val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor
+      val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.unit).toInt)
 
       val snapshot = current_base_snapshot
       val results = current_base_results
diff -r 874e12fb6c3d -r 4e3d461afa10 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 13:55:54 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 14:44:29 2024 +0100
@@ -247,10 +247,9 @@
       val painter = pretty_text_area.getPainter
       val geometry = JEdit_Lib.window_geometry(pretty_tooltip, painter)
       val metric = JEdit_Lib.font_metric(painter)
-
       val margin =
-        ((rendering.tooltip_margin * metric.average) min
-          ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
+        metric.pretty_margin(rendering.tooltip_margin,
+          limit = ((w_max - geometry.deco_width) / metric.unit).floor)
 
       val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
       val lines = XML.content_lines(formatted)