# HG changeset patch
# User wenzelm
# Date 1731074916 -3600
# Node ID 5f401c2f7d333dbad3424df9be88f27b0ea33068
# Parent  4e3d461afa105b02d79af4a8c4d7cbb0b0c4f9c7
more accurate pretty_margin for proportional fonts;

diff -r 4e3d461afa10 -r 5f401c2f7d33 src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Fri Nov 08 14:44:29 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Fri Nov 08 15:08:36 2024 +0100
@@ -55,8 +55,8 @@
   }
   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
+  def pretty_margin(margin: Int, limit: Int = -1): Int = {
+    val m = (margin * average).toInt
+    (if (limit < 0) m else m min limit) max 20
   }
 }
diff -r 4e3d461afa10 -r 5f401c2f7d33 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 14:44:29 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 15:08:36 2024 +0100
@@ -88,7 +88,7 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.font_metric(getPainter)
-      val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.unit).toInt)
+      val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.average_width).toInt)
 
       val snapshot = current_base_snapshot
       val results = current_base_results
diff -r 4e3d461afa10 -r 5f401c2f7d33 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 14:44:29 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 15:08:36 2024 +0100
@@ -249,7 +249,7 @@
       val metric = JEdit_Lib.font_metric(painter)
       val margin =
         metric.pretty_margin(rendering.tooltip_margin,
-          limit = ((w_max - geometry.deco_width) / metric.unit).floor)
+          limit = ((w_max - geometry.deco_width) / metric.average_width).toInt)
 
       val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
       val lines = XML.content_lines(formatted)
@@ -259,7 +259,7 @@
         if (h <= h_max) {
           split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
         }
-        else margin
+        else margin.toDouble
       val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
 
       new Dimension(w min w_max, h min h_max)