# HG changeset patch
# User wenzelm
# Date 1731081468 -3600
# Node ID c519a14bd3f6c5f412ef350f79c48bf1c9b3e818
# Parent  7acc6fabca6adb6ec00f0ac71d77c3a501321b6d
tuned GUI: avoid wasting space with proportional fonts;

diff -r 7acc6fabca6a -r c519a14bd3f6 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 16:52:06 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 16:57:48 2024 +0100
@@ -260,7 +260,7 @@
           split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
         }
         else margin.toDouble
-      val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
+      val w = (metric.unit * (margin1 + 1)).round.toInt + geometry.deco_width
 
       new Dimension(w min w_max, h min h_max)
     }