--- 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
}
}
--- 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
--- 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)