--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Mar 04 15:41:46 2021 +0100
@@ -267,7 +267,7 @@
val h = painter.getLineHeight * lines + geometry.deco_height
val margin1 =
if (h <= h_max) {
- split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+ split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
}
else margin
val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width